diff options
Diffstat (limited to 'doc/sphinx/user-extensions')
| -rw-r--r-- | doc/sphinx/user-extensions/proof-schemes.rst | 10 | ||||
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 21 |
2 files changed, 18 insertions, 13 deletions
diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst index 5b0b3c51b0..34197c4fcf 100644 --- a/doc/sphinx/user-extensions/proof-schemes.rst +++ b/doc/sphinx/user-extensions/proof-schemes.rst @@ -337,31 +337,31 @@ Generation of inversion principles with ``Derive`` ``Inversion`` ----------------------------------------------------------------- .. cmd:: Derive Inversion @ident with @ident Sort @sort - Derive Inversion @ident with (forall @binders, @ident @term) Sort @sort + Derive Inversion @ident with (forall {* @binder }, @ident @term) Sort @sort This command generates an inversion principle for the :tacn:`inversion ... using ...` tactic. The first :token:`ident` is the name of the generated principle. The second :token:`ident` should be an inductive predicate, and :token:`binders` the variables occurring in the term :token:`term`. This command generates the inversion lemma for the sort - :token:`sort` corresponding to the instance :n:`forall @binders, @ident @term`. + :token:`sort` corresponding to the instance :n:`forall {* @binder }, @ident @term`. When applied, it is equivalent to having inverted the instance with the tactic :g:`inversion`. .. cmdv:: Derive Inversion_clear @ident with @ident Sort @sort - Derive Inversion_clear @ident with (forall @binders, @ident @term) Sort @sort + Derive Inversion_clear @ident with (forall {* @binder }, @ident @term) Sort @sort When applied, it is equivalent to having inverted the instance with the tactic inversion replaced by the tactic `inversion_clear`. .. cmdv:: Derive Dependent Inversion @ident with @ident Sort @sort - Derive Dependent Inversion @ident with (forall @binders, @ident @term) Sort @sort + Derive Dependent Inversion @ident with (forall {* @binder }, @ident @term) Sort @sort When applied, it is equivalent to having inverted the instance with the tactic `dependent inversion`. .. cmdv:: Derive Dependent Inversion_clear @ident with @ident Sort @sort - Derive Dependent Inversion_clear @ident with (forall @binders, @ident @term) Sort @sort + Derive Dependent Inversion_clear @ident with (forall {* @binder }, @ident @term) Sort @sort When applied, it is equivalent to having inverted the instance with the tactic `dependent inversion_clear`. diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index c568f13c12..fd95a5cef4 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -310,10 +310,10 @@ at the time of use of the notation. The Infix command ~~~~~~~~~~~~~~~~~~ -The :cmd:`Infix` command is a shortening for declaring notations of infix +The :cmd:`Infix` command is a shortcut for declaring notations for infix symbols. -.. cmd:: Infix "@symbol" := @term {? (@modifiers) }. +.. cmd:: Infix @string := @term {? (@modifiers) } This command is equivalent to @@ -366,7 +366,7 @@ Thanks to reserved notations, the inductive, co-inductive, record, recursive and corecursive definitions can benefit from customized notations. To do this, insert a ``where`` notation clause after the definition of the (co)inductive type or (co)recursive term (or after the definition of each of them in case of mutual -definitions). The exact syntax is given by :token:`decl_notation` for inductive, +definitions). The exact syntax is given by :n:`@decl_notation` for inductive, co-inductive, recursive and corecursive definitions and in :ref:`record-types` for records. Here are examples: @@ -909,12 +909,11 @@ notations are given below. The optional :production:`scope` is described in notation : [Local] Notation `string` := `term` [(`modifiers`)] [: `scope`]. : [Local] Infix `string` := `qualid` [(`modifiers`)] [: `scope`]. : [Local] Reserved Notation `string` [(`modifiers`)] . - : Inductive `ind_body` [`decl_notation`] with … with `ind_body` [`decl_notation`]. - : CoInductive `ind_body` [`decl_notation`] with … with `ind_body` [`decl_notation`]. - : Fixpoint `fix_body` [`decl_notation`] with … with `fix_body` [`decl_notation`]. - : CoFixpoint `fix_body` [`decl_notation`] with … with `fix_body` [`decl_notation`]. + : Inductive `ind_body` [`decl_notations`] with … with `ind_body` [`decl_notations`]. + : CoInductive `ind_body` [`decl_notations`] with … with `ind_body` [`decl_notations`]. + : Fixpoint `fix_body` [`decl_notations`] with … with `fix_body` [`decl_notations`]. + : CoFixpoint `fix_body` [`decl_notations`] with … with `fix_body` [`decl_notations`]. : [Local] Declare Custom Entry `ident`. - decl_notation : [where `string` := `term` [: `scope`] and … and `string` := `term` [: `scope`]]. modifiers : `modifier`, … , `modifier` modifier : at level `num` : in custom `ident` @@ -944,6 +943,12 @@ notations are given below. The optional :production:`scope` is described in : as pattern : as strict pattern +.. insertprodn decl_notations decl_notation + +.. prodn:: + decl_notations ::= where @decl_notation {* and @decl_notation } + decl_notation ::= @string := @term1_extended [(only parsing)] {? : @ident } + .. note:: No typing of the denoted expression is performed at definition time. Type checking is done only at the time of use of the notation. |