diff options
Diffstat (limited to 'doc/sphinx/addendum')
| -rw-r--r-- | doc/sphinx/addendum/extraction.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/addendum/generalized-rewriting.rst | 25 | ||||
| -rw-r--r-- | doc/sphinx/addendum/program.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/addendum/type-classes.rst | 39 |
4 files changed, 28 insertions, 40 deletions
diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst index e93b01f14d..8a895eb515 100644 --- a/doc/sphinx/addendum/extraction.rst +++ b/doc/sphinx/addendum/extraction.rst @@ -99,7 +99,7 @@ Extraction Options Setting the target language ~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. cmd:: Extraction Language ( OCaml | Haskell | Scheme ) +.. cmd:: Extraction Language {| OCaml | Haskell | Scheme } :name: Extraction Language The ability to fix target language is the first and more important diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index b474c51f17..847abb33fc 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -170,12 +170,12 @@ compatibility constraints. Adding new relations and morphisms ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. cmd:: Add Parametric Relation (x1 : T1) ... (xn : Tk) : (A t1 ... tn) (Aeq t′1 ... t′m) {? reflexivity proved by refl} {? symmetry proved by sym} {? transitivity proved by trans} as @ident +.. cmd:: Add Parametric Relation @binders : (A t1 ... tn) (Aeq t′1 ... t′m) {? reflexivity proved by @term} {? symmetry proved by @term} {? transitivity proved by @term} as @ident This command declares a parametric relation :g:`Aeq: forall (y1 : β1 ... ym : βm)`, :g:`relation (A t1 ... tn)` over :g:`(A : αi -> ... αn -> Type)`. - The :token:`ident` gives a unique name to the morphism and it is used + The final :token:`ident` gives a unique name to the morphism and it is used by the command to generate fresh names for automatically provided lemmas used internally. @@ -219,15 +219,16 @@ replace terms with related ones only in contexts that are syntactic compositions of parametric morphism instances declared with the following command. -.. cmd:: Add Parametric Morphism (x1 : T1) ... (xk : Tk) : (f t1 ... tn) with signature sig as @ident +.. cmd:: Add Parametric Morphism @binders : (@ident {+ @term__1}) with signature @term__2 as @ident - This command declares ``f`` as a parametric morphism of signature ``sig``. The - identifier :token:`ident` gives a unique name to the morphism and it is used as - the base name of the typeclass instance definition and as the name of - the lemma that proves the well-definedness of the morphism. The - parameters of the morphism as well as the signature may refer to the - context of variables. The command asks the user to prove interactively - that ``f`` respects the relations identified from the signature. + This command declares a parametric morphism :n:`@ident {+ @term__1}` of + signature :n:`@term__2`. The final identifier :token:`ident` gives a unique + name to the morphism and it is used as the base name of the typeclass + instance definition and as the name of the lemma that proves the + well-definedness of the morphism. The parameters of the morphism as well as + the signature may refer to the context of variables. The command asks the + user to prove interactively that the function denoted by the first + :token:`ident` respects the relations identified from the signature. .. example:: @@ -577,7 +578,7 @@ Deprecated syntax and backward incompatibilities Notice that the syntax is not completely backward compatible since the identifier was not required. -.. cmd:: Add Morphism f : @ident +.. cmd:: Add Morphism @ident : @ident :name: Add Morphism This command is restricted to the declaration of morphisms @@ -809,7 +810,7 @@ Usage ~~~~~ -.. tacn:: rewrite_strat @s [in @ident] +.. tacn:: rewrite_strat @s {? in @ident } :name: rewrite_strat Rewrite using the strategy s in hypothesis ident or the conclusion. diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index b410833d25..22ddcae584 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -283,7 +283,7 @@ optional identifier is used when multiple functions have unsolved obligations (e.g. when defining mutually recursive blocks). The optional tactic is replaced by the default one if not specified. -.. cmd:: {? Local|Global} Obligation Tactic := @tactic +.. cmd:: {? {| Local | Global } } Obligation Tactic := @tactic :name: Obligation Tactic Sets the default obligation solving tactic applied to all obligations diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index 77a6ee79cc..65934efaa6 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -311,24 +311,24 @@ Summary of the commands This command has no effect when used on a typeclass. -.. cmd:: Instance @ident {? @binders} : @class t1 … tn [| priority] := { field1 := b1 ; …; fieldi := bi } +.. cmd:: Instance @ident {? @binders} : @term__0 {+ @term} {? | @num} := { {*; @field_def} } This command is used to declare a typeclass instance named - :token:`ident` of the class :token:`class` with parameters ``t1`` to ``tn`` and - fields ``b1`` to ``bi``, where each field must be a declared field of - the class. Missing fields must be filled in interactive proof mode. + :token:`ident` of the class :n:`@term__0` with parameters :token:`term` and + fields defined by :token:`field_def`, where each field must be a declared field of + the class. An arbitrary context of :token:`binders` can be put after the name of the instance and before the colon to declare a parameterized instance. An optional priority can be declared, 0 being the highest priority as for - :tacn:`auto` hints. If the priority is not specified, it defaults to the number + :tacn:`auto` hints. If the priority :token:`num` is not specified, it defaults to the number of non-dependent binders of the instance. - .. cmdv:: Instance @ident {? @binders} : forall {? @binders}, @class @term__1 … @term__n [| priority] := @term + .. cmdv:: Instance @ident {? @binders} : forall {? @binders}, @term__0 {+ @term} {? | @num } := @term This syntax is used for declaration of singleton class instances or - for directly giving an explicit term of type :n:`forall @binders, @class - @term__1 … @term__n`. One need not even mention the unique field name for + for directly giving an explicit term of type :n:`forall @binders, @term__0 + {+ @term}`. One need not even mention the unique field name for singleton classes. .. cmdv:: Global Instance @@ -356,11 +356,11 @@ Summary of the commands Besides the :cmd:`Class` and :cmd:`Instance` vernacular commands, there are a few other commands related to typeclasses. -.. cmd:: Existing Instance {+ @ident} [| priority] +.. cmd:: Existing Instance {+ @ident} {? | @num} This command adds an arbitrary list of constants whose type ends with an applied typeclass to the instance database with an optional - priority. It can be used for redeclaring instances at the end of + priority :token:`num`. It can be used for redeclaring instances at the end of sections, or declaring structure projections as instances. This is equivalent to ``Hint Resolve ident : typeclass_instances``, except it registers instances for :cmd:`Print Instances`. @@ -408,7 +408,7 @@ few other commands related to typeclasses. + When considering local hypotheses, we use the union of all the modes declared in the given databases. - .. cmdv:: typeclasses eauto @num + .. tacv:: typeclasses eauto @num .. warning:: The semantics for the limit :n:`@num` @@ -417,7 +417,7 @@ few other commands related to typeclasses. counted, which might result in larger limits being necessary when searching with ``typeclasses eauto`` than with :tacn:`auto`. - .. cmdv:: typeclasses eauto with {+ @ident} + .. tacv:: typeclasses eauto with {+ @ident} This variant runs resolution with the given hint databases. It treats typeclass subgoals the same as other subgoals (no shelving of @@ -563,23 +563,10 @@ Settings of goals. Setting this option to 1 or 2 turns on :flag:`Typeclasses Debug`; setting this option to 0 turns that option off. -.. flag:: Refine Instance Mode - - .. deprecated:: 8.10 - - This flag allows to switch the behavior of instance declarations made through - the Instance command. - - + When it is off (the default), they fail with an error instead. - - + When it is on, instances that have unsolved holes in - their proof-term silently open the proof mode with the remaining - obligations to prove. - Typeclasses eauto `:=` ~~~~~~~~~~~~~~~~~~~~~~ -.. cmd:: Typeclasses eauto := {? debug} {? (dfs) | (bfs) } @num +.. cmd:: Typeclasses eauto := {? debug} {? {| (dfs) | (bfs) } } @num :name: Typeclasses eauto This command allows more global customization of the typeclass |