Stream: math-comp users

Topic: finfun / dfinfun


view this post on Zulip 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.

view this post on Zulip Cyril Cohen (Mar 02 2021 at 10:41):

https://github.com/math-comp/math-comp/blob/17dd3091e7f809c1385b0c0be43d1f8de4fa6be0/mathcomp/ssreflect/finfun.v#L18-L21

view this post on Zulip 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...

view this post on Zulip Pierre-Yves Strub (Mar 02 2021 at 10:43):

That would be super useful. Or adding notations for [ffun ...] that go in dffun.

view this post on Zulip Pierre-Yves Strub (Mar 02 2021 at 10:43):

Otherwise, you end adding a lot of type annotations.

view this post on Zulip Cyril Cohen (Mar 02 2021 at 10:43):

Would you mind opening an issue about this?

view this post on Zulip Cyril Cohen (Mar 02 2021 at 10:44):

Pierre-Yves Strub said:

That would be super useful. Or adding notations for [ffun ...] that go in dffun.

The latter is obviously simpler to do a posteriori

view this post on Zulip Pierre-Yves Strub (Mar 02 2021 at 10:45):

I am opening a ticket


Last updated: Feb 08 2023 at 07:02 UTC