diff options
Diffstat (limited to 'plugins/micromega')
| -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. |