Quinn (Nov 09 2021 at 14:43): Quinn (Nov 09 2021 at 14:43):@Gaëtan Gilbert writes
fixpoints are forbidden on variants since https://github.com/coq/coq/pull/407 (as a side effect of forbidding fixpoints on records with eta)
What's a record with eta?
Gaëtan Gilbert (Nov 09 2021 at 14:44):https://coq.github.io/doc/master/refman/language/core/records.html#primitive-projections bullet point 1
Quinn (Nov 09 2021 at 14:52):ok, thanks
Last updated: Oct 03 2023 at 04:02 UTC