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/Bool | |
| 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/Bool')
| -rw-r--r-- | theories/Bool/Bool.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index d70978fabe..9e10786fcd 100644 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -130,6 +130,8 @@ Definition eqb (b1 b2:bool) : bool := | false, false => true end. +Register eqb as core.bool.eqb. + Lemma eqb_subst : forall (P:bool -> Prop) (b1 b2:bool), eqb b1 b2 = true -> P b1 -> P b2. Proof. |