Stream: Coq users

Topic: ✔ Meaning of 'struct'


view this post on Zulip Patrick Nicodemus (May 29 2022 at 06:29):

https://coq.inria.fr/refman/language/extensions/match.html
What is the meaning of the struct keyword in the definitions on this page? Where can I find the documentation for this?

view this post on Zulip Gaëtan Gilbert (May 29 2022 at 08:22):

https://coq.inria.fr/refman/language/core/inductive.html#grammar-token-fixannot

To be accepted, a Fixpoint definition has to satisfy syntactical constraints on a special argument called the decreasing argument. They are needed to ensure that the Fixpoint definition always terminates. The point of the {struct ident} annotation (see fixannot) is to let the user tell the system which argument decreases along the recursive calls.

view this post on Zulip Notification Bot (May 29 2022 at 08:25):

Patrick Nicodemus has marked this topic as resolved.


Last updated: Jun 20 2024 at 12:02 UTC