diff options
Diffstat (limited to 'doc/sphinx/addendum')
| -rw-r--r-- | doc/sphinx/addendum/extraction.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/addendum/micromega.rst | 29 | ||||
| -rw-r--r-- | doc/sphinx/addendum/nsatz.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/addendum/program.rst | 11 | ||||
| -rw-r--r-- | doc/sphinx/addendum/type-classes.rst | 22 |
5 files changed, 36 insertions, 32 deletions
diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst index ce68274036..c2249b8e57 100644 --- a/doc/sphinx/addendum/extraction.rst +++ b/doc/sphinx/addendum/extraction.rst @@ -429,11 +429,11 @@ Additional settings Provides a comment that is included at the beginning of the output files. -.. opt:: Extraction Flag @num +.. opt:: Extraction Flag @natural :name: Extraction Flag Controls which optimizations are used during extraction, providing a finer-grained - control than :flag:`Extraction Optimize`. The bits of :token:`num` are used as a bit mask. + control than :flag:`Extraction Optimize`. The bits of :token:`natural` are used as a bit mask. Keeping an option off keeps the extracted ML more similar to the Coq term. Values are: diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index 070e899c9d..ba5bac6489 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -61,19 +61,23 @@ tactics for solving arithmetic goals over :math:`\mathbb{Q}`, The tactics solve propositional formulas parameterized by atomic arithmetic expressions interpreted over a domain :math:`D \in \{\mathbb{Z},\mathbb{Q},\mathbb{R}\}`. -The syntax of the formulas is the following: +The syntax for formulas over :math:`\mathbb{Z}` is: - .. productionlist:: F - F : A ∣ P | True ∣ False ∣ F ∧ F ∣ F ∨ F ∣ F ↔ F ∣ F → F ∣ ¬ F | F = F - A : p = p ∣ p > p ∣ p < p ∣ p ≥ p ∣ p ≤ p - p : c ∣ x ∣ −p ∣ p − p ∣ p + p ∣ p × p ∣ p ^ n + .. note the following is not an insertprodn -where :math:`F` is interpreted over either `Prop` or `bool`, -:math:`c` is a numeric constant, :math:`x \in D` is a numeric variable, the -operators :math:`−, +, ×` are respectively subtraction, addition, and product; -:math:`p ^ n` is exponentiation by a constant :math:`n`, :math:`P` is an arbitrary proposition. -For :math:`\mathbb{Q}`, equality is not Leibniz equality ``=`` but the equality of -rationals ``==``. + .. prodn:: + F ::= {| @A | P | True | False | @F /\\ @F | @F \\/ @F | @F <-> @F | @F -> @F | ~ @F | @F = @F } + A ::= {| @p = @p | @p > @p | @p < @p | @p >= @p | @p <= @p } + p ::= {| c | x | −@p | @p − @p | @p + @p | @p * @p | @p ^ n } + +where + + - :token:`F` is interpreted over either `Prop` or `bool` + - :n:`P` is an arbitrary proposition + - :n:`c` is a numeric constant of :math:`D` + - :n:`x` :math:`\in D` is a numeric variable + - :n:`−`, :n:`+` and :n:`*` are respectively subtraction, addition and product + - :n:`p ^ n` is exponentiation by a constant :math:`n` When :math:`F` is interpreted over `bool`, the boolean operators are `&&`, `||`, `Bool.eqb`, `Bool.implb`, `Bool.negb` and the comparisons @@ -81,6 +85,9 @@ in :math:`A` are also interpreted over the booleans (e.g., for :math:`\mathbb{Z}`, we have `Z.eqb`, `Z.gtb`, `Z.ltb`, `Z.geb`, `Z.leb`). +For :math:`\mathbb{Q}`, use the equality of rationals ``==`` rather than +Leibniz equality ``=``. + For :math:`\mathbb{Z}` (resp. :math:`\mathbb{Q}`), :math:`c` ranges over integer constants (resp. rational constants). For :math:`\mathbb{R}`, the tactic recognizes as real constants the following expressions: diff --git a/doc/sphinx/addendum/nsatz.rst b/doc/sphinx/addendum/nsatz.rst index ed93145622..8a64a7ed4b 100644 --- a/doc/sphinx/addendum/nsatz.rst +++ b/doc/sphinx/addendum/nsatz.rst @@ -64,7 +64,7 @@ Buchberger algorithm. This computation is done after a step of *reification*, which is performed using :ref:`typeclasses`. -.. tacv:: nsatz with radicalmax:=@num%N strategy:=@num%Z parameters:=[{*, @ident}] variables:=[{*, @ident}] +.. tacv:: nsatz with radicalmax:=@natural%N strategy:=@natural%Z parameters:=[{*, @ident}] variables:=[{*, @ident}] Most complete syntax for `nsatz`. diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index b5618c5721..c6a4b4fe1a 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -196,12 +196,9 @@ Program Definition Program Fixpoint ~~~~~~~~~~~~~~~~ -.. cmd:: Program Fixpoint @ident {* @binder } {? {@order}} : @type := @term +.. cmd:: Program Fixpoint @fix_definition {* with @fix_definition } - The optional order annotation follows the grammar: - - .. productionlist:: orderannot - order : measure `term` [ `term` ] | wf `term` `ident` + The optional :n:`@fixannot` annotation can be one of: + :g:`measure f R` where :g:`f` is a value of type :g:`X` computed on any subset of the arguments and the optional term @@ -306,9 +303,9 @@ optional tactic is replaced by the default one if not specified. Displays all remaining obligations. -.. cmd:: Obligation @num {? of @ident} +.. cmd:: Obligation @natural {? of @ident} - Start the proof of obligation :token:`num`. + Start the proof of obligation :token:`natural`. .. cmd:: Next Obligation {? of @ident} diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index 903aa266e2..11162ec96b 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -330,7 +330,7 @@ Summary of the commands This command has no effect when used on a typeclass. -.. cmd:: Instance @ident {* @binder } : @term__0 {+ @term} {? | @num} := { {*; @field_def} } +.. cmd:: Instance @ident {* @binder } : @term__0 {+ @term} {? | @natural} := { {*; @field_def} } This command is used to declare a typeclass instance named :token:`ident` of the class :n:`@term__0` with parameters :token:`term` and @@ -340,7 +340,7 @@ Summary of the commands 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 :token:`num` is not specified, it defaults to the number + :tacn:`auto` hints. If the priority :token:`natural` is not specified, it defaults to the number of non-dependent binders of the instance. This command supports the :attr:`global` attribute that can be @@ -362,7 +362,7 @@ Summary of the commands to fill them. It works exactly as if no body had been given and the :tacn:`refine` tactic has been used first. - .. cmdv:: Instance @ident {* @binder } : forall {* @binder }, @term__0 {+ @term} {? | @num } := @term + .. cmdv:: Instance @ident {* @binder } : forall {* @binder }, @term__0 {+ @term} {? | @natural } := @term This syntax is used for declaration of singleton class instances or for directly giving an explicit term of type :n:`forall {* @binder }, @term__0 @@ -381,11 +381,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} {? | @num} +.. cmd:: Existing Instance {+ @ident} {? | @natural} This command adds an arbitrary list of constants whose type ends with an applied typeclass to the instance database with an optional - priority :token:`num`. It can be used for redeclaring instances at the end of + priority :token:`natural`. 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`. @@ -446,10 +446,10 @@ few other commands related to typeclasses. + When considering local hypotheses, we use the union of all the modes declared in the given databases. - .. tacv:: typeclasses eauto @num + .. tacv:: typeclasses eauto @natural .. warning:: - The semantics for the limit :n:`@num` + The semantics for the limit :n:`@natural` is different than for auto. By default, if no limit is given, the search is unbounded. Contrary to :tacn:`auto`, introduction steps are counted, which might result in larger limits being necessary when @@ -581,7 +581,7 @@ Settings Otherwise, the search strategy is depth-first search. The default is off. :cmd:`Typeclasses eauto` is another way to set this flag. -.. opt:: Typeclasses Depth @num +.. opt:: Typeclasses Depth @natural :name: Typeclasses Depth Sets the maximum proof search depth. The default is unbounded. @@ -593,7 +593,7 @@ Settings also sets :opt:`Typeclasses Debug Verbosity` to 1. :cmd:`Typeclasses eauto` is another way to set this flag. -.. opt:: Typeclasses Debug Verbosity @num +.. opt:: Typeclasses Debug Verbosity @natural :name: Typeclasses Debug Verbosity Determines how much information is shown for typeclass resolution steps during search. @@ -604,7 +604,7 @@ Settings Typeclasses eauto `:=` ~~~~~~~~~~~~~~~~~~~~~~ -.. cmd:: Typeclasses eauto := {? debug} {? {| (dfs) | (bfs) } } @num +.. cmd:: Typeclasses eauto := {? debug} {? {| (dfs) | (bfs) } } @natural :name: Typeclasses eauto This command allows more global customization of the typeclass @@ -618,5 +618,5 @@ Typeclasses eauto `:=` search (the default) or breadth-first search. The search strategy can also be set with :flag:`Typeclasses Iterative Deepening`. - + :token:`num` This sets the depth limit of the search. The depth + + :token:`natural` This sets the depth limit of the search. The depth limit can also be set with :opt:`Typeclasses Depth`. |