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 https://github.com/coq/coq/pull/13107


Last updated: Jan 27 2023 at 00:03 UTC