Pierre-Yves Strub (Mar 02 2021 at 10:35): Pierre-Yves Strub (Mar 02 2021 at 10:35):Is there a reason why finfun is only equipped with an eqType for the non-dependent version? I find these ffun / dffun quite hard to work with.
Cyril Cohen (Mar 02 2021 at 10:41): Cyril Cohen (Mar 02 2021 at 10:42):We should check whether the problem that Georges reported back then about Coq 8.9 unification mechanizm is still actual and if not merge ffun and dffun...
Pierre-Yves Strub (Mar 02 2021 at 10:43):That would be super useful. Or adding notations for [ffun ...] that go in dffun.
Pierre-Yves Strub (Mar 02 2021 at 10:43):Otherwise, you end adding a lot of type annotations.
Cyril Cohen (Mar 02 2021 at 10:43):Would you mind opening an issue about this?
Cyril Cohen (Mar 02 2021 at 10:44):Pierre-Yves Strub said:
That would be super useful. Or adding notations for
[ffun ...]that go indffun.
The latter is obviously simpler to do a posteriori
Pierre-Yves Strub (Mar 02 2021 at 10:45):I am opening a ticket
Last updated: Oct 13 2024 at 01:02 UTC