Stream: Coq users

Topic: Bidirectionality hint, better defaults?

view this post on Zulip Li-yao (Nov 06 2021 at 17:16):

I often find myself putting bidirectionality hints (Arguments f _ & _.) on constructors right after their parameters. I know only the bare minimum about bidirectional type checking, but wouldn't it be nice if that happened by default when declaring a type, or are there good reasons for the current behavior?

view this post on Zulip Gaëtan Gilbert (Nov 06 2021 at 17:19):

changing it breaks backwards compat
also bidi can produce "too reduced" terms depending on what unification problems come up
see also

Last updated: Jun 15 2024 at 05:01 UTC