diff options
| author | Frédéric Besson | 2020-05-11 11:59:42 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2020-06-14 11:26:41 +0200 |
| commit | f8e91cb0a227a2d0423412e7533163568e1e9fdf (patch) | |
| tree | 3a16a91e7167cb942686ab6657b76e3b86c151df /theories/ZArith | |
| parent | 13e8d04b2f080fbc7ca169bc39e53c8dd091d279 (diff) | |
[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.
Diffstat (limited to 'theories/ZArith')
| -rw-r--r-- | theories/ZArith/BinInt.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index 1729b9f85e..a566348dd5 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -47,6 +47,8 @@ Register mul as num.Z.mul. Register pow as num.Z.pow. Register of_nat as num.Z.of_nat. + + (** When including property functors, only inline t eq zero one two *) Set Inline Level 30. @@ -81,6 +83,11 @@ Register le as num.Z.le. Register lt as num.Z.lt. Register ge as num.Z.ge. Register gt as num.Z.gt. +Register leb as num.Z.leb. +Register ltb as num.Z.ltb. +Register geb as num.Z.geb. +Register gtb as num.Z.gtb. +Register eqb as num.Z.eqb. (** * Decidability of equality. *) |