Gaëtan Gilbert (May 29 2022 at 08:22): 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: Feb 08 2023 at 22:03 UTC