Patrick Nicodemus (May 29 2022 at 06:29): 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?
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.
Notification Bot (May 29 2022 at 08:25):Patrick Nicodemus has marked this topic as resolved.
Last updated: Oct 04 2023 at 20:01 UTC