diff options
| author | coqbot-app[bot] | 2020-10-25 20:00:32 +0000 |
|---|---|---|
| committer | GitHub | 2020-10-25 20:00:32 +0000 |
| commit | a12112c15cdcb0467d4cf5f5a7cfa639852ccd49 (patch) | |
| tree | 3e2d8983efe06e93cbfab75a65b4f4420525332a /doc/sphinx/language/core/inductive.rst | |
| parent | d397f10bf4d334189523e187b2cd5fd6e18b4bcc (diff) | |
| parent | 7a57a23e4fb8a74e8746d4eaee900f2ced37a28a (diff) | |
Merge PR #12936: Convert misc chapters to prodn, update syntax
Reviewed-by: Zimmi48
Ack-by: mattam82
Ack-by: pi8027
Ack-by: herbelin
Ack-by: gares
Ack-by: fajb
Ack-by: proux01
Diffstat (limited to 'doc/sphinx/language/core/inductive.rst')
| -rw-r--r-- | doc/sphinx/language/core/inductive.rst | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst index 0b18c9dcf1..122b0f5dfb 100644 --- a/doc/sphinx/language/core/inductive.rst +++ b/doc/sphinx/language/core/inductive.rst @@ -361,7 +361,11 @@ syntax: :n:`let fix @ident {* @binder } := @term in` stands for Some options of :n:`@fixannot` are only supported in specific constructs. :n:`fix` and :n:`let fix` only support the :n:`struct` option, while :n:`wf` and :n:`measure` are only supported in -commands such as :cmd:`Function` and :cmd:`Program Fixpoint`. +commands such as :cmd:`Fixpoint` (with the :attr:`program` attribute) and :cmd:`Function`. + +.. todo explanation of struct: see text above at the Fixpoint command, also + see https://github.com/coq/coq/pull/12936#discussion_r510716268 and above. + Consider whether to move the grammar for fixannot elsewhere .. _Fixpoint: @@ -379,7 +383,7 @@ constructions. .. prodn:: fix_definition ::= @ident_decl {* @binder } {? @fixannot } {? : @type } {? := @term } {? @decl_notations } - This command allows defining functions by pattern matching over inductive + Allows defining functions by pattern matching over inductive objects using a fixed point construction. The meaning of this declaration is to define :n:`@ident` as a recursive function with arguments specified by the :n:`@binder`\s such that :n:`@ident` applied to arguments @@ -388,6 +392,8 @@ constructions. consequently :n:`forall {* @binder }, @type` and its value is equivalent to :n:`fun {* @binder } => @term`. + This command accepts the :attr:`program` attribute. + To be accepted, a :cmd:`Fixpoint` definition has to satisfy syntactical constraints on a special argument called the decreasing argument. They are needed to ensure that the :cmd:`Fixpoint` definition always terminates. @@ -399,7 +405,7 @@ constructions. that satisfies the decreasing condition. :cmd:`Fixpoint` without the :attr:`program` attribute does not support the - :n:`wf` or :n:`measure` clauses of :n:`@fixannot`. + :n:`wf` or :n:`measure` clauses of :n:`@fixannot`. See :ref:`program_fixpoint`. The :n:`with` clause allows simultaneously defining several mutual fixpoints. It is especially useful when defining functions over mutually defined |