From f8e91cb0a227a2d0423412e7533163568e1e9fdf Mon Sep 17 00:00:00 2001
From: Frédéric Besson
Date: Mon, 11 May 2020 11:59:42 +0200
Subject: [micromega] native support for boolean operators

The syntax of formulae is extended to support boolean constants (true,
false), boolean operators Bool.andb, Bool.orb, Bool.implb, Bool.negb,
Bool.eqb and comparison operators Z.eqb, Z.ltb, Z.gtb, Z.leb and
Z.ltb.
---
 doc/sphinx/addendum/micromega.rst | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

(limited to 'doc/sphinx')

diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index 77bf58aac6..717b0deb43 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -64,16 +64,23 @@ arithmetic expressions interpreted over a domain :math:`D \in \{\mathbb{Z},\math
 The syntax of the formulas is the following:
 
  .. productionlist:: F
-   F : A ∣ P ∣ True ∣ False ∣ F ∧ F ∣ F ∨ F ∣ F ↔ F ∣ F → F ∣ ¬ 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
 
-where :math:`c` is a numeric constant, :math:`x \in D` is a numeric variable, the
+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 ``==``.
 
+When :math:`F` is interpreted over `bool`, the boolean operators are
+`&&`, `||`, `Bool.eqb`, `Bool.implb`, `Bool.negb` and the comparisons
+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{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:
-- 
cgit v1.2.3