Stream: Coq users

Topic: Records with eta


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Quinn (Nov 09 2021 at 14:52):

ok, thanks


Last updated: Feb 08 2023 at 23:03 UTC