Li-yao (Nov 06 2021 at 17:16): 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?
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: Sep 23 2023 at 13:01 UTC