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/Init | |
| 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/Init')
| -rw-r--r-- | theories/Init/Datatypes.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index cba90043d5..8ab12ae534 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -73,6 +73,7 @@ Infix "&&" := andb : bool_scope. Register andb as core.bool.andb. Register orb as core.bool.orb. +Register implb as core.bool.implb. Register xorb as core.bool.xorb. Register negb as core.bool.negb. |