Stream: Coq users

Topic: ✔ Meaning of 'struct'


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: Feb 08 2023 at 22:03 UTC