diff options
| author | Frédéric Besson | 2019-10-25 19:29:03 +0200 |
|---|---|---|
| committer | Frédéric Besson | 2019-10-25 19:29:03 +0200 |
| commit | f7659e6c5d197ddeff8509a4aab40316534b3a12 (patch) | |
| tree | 4d5f170c62799ac0e4dd830f4412e3a6477e8bd5 /plugins | |
| parent | 6ed3b02af77313d62ec868b4a88a208a9003857d (diff) | |
| parent | de05e0e6e3869973a5a1dd5427748c3918a6a23d (diff) | |
Merge PR #10962: Add missing instances for `implb` and `xorb` in ZifyBool.v
Reviewed-by: fajb
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/micromega/ZifyBool.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/plugins/micromega/ZifyBool.v b/plugins/micromega/ZifyBool.v index 03a7774a31..b94b74097b 100644 --- a/plugins/micromega/ZifyBool.v +++ b/plugins/micromega/ZifyBool.v @@ -42,6 +42,16 @@ Instance Op_orb : BinOp orb := TBOpInj := ltac:(destruct n,m; reflexivity)}. Add BinOp Op_orb. +Instance Op_implb : BinOp implb := + { TBOp := fun x y => Z.max (1 - x) y; + TBOpInj := ltac:(destruct n,m; reflexivity) }. +Add BinOp Op_implb. + +Instance Op_xorb : BinOp xorb := + { TBOp := fun x y => Z.max (x - y) (y - x); + TBOpInj := ltac:(destruct n,m; reflexivity) }. +Add BinOp Op_xorb. + Instance Op_negb : UnOp negb := { TUOp := fun x => 1 - x ; TUOpInj := ltac:(destruct x; reflexivity)}. Add UnOp Op_negb. |