diff options
Diffstat (limited to 'doc/sphinx/addendum')
| -rw-r--r-- | doc/sphinx/addendum/micromega.rst | 29 | ||||
| -rw-r--r-- | doc/sphinx/addendum/program.rst | 7 |
2 files changed, 20 insertions, 16 deletions
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/program.rst b/doc/sphinx/addendum/program.rst index b5618c5721..3d36c5c50f 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 |