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?
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