diff options
| author | Frédéric Besson | 2019-11-16 14:54:42 +0100 |
|---|---|---|
| committer | Frédéric Besson | 2019-11-16 14:54:42 +0100 |
| commit | 6045fcf7398c4098566f7da5c4cba808c7416788 (patch) | |
| tree | c4cf05c9fe17d6ff456a2de404d65cf70ff95009 /plugins/micromega/ZifyBool.v | |
| parent | 622b4f3ace40313d8dc17141285da32de80b3183 (diff) | |
| parent | 64a5f8f4e803971eac858a2f1dbb748c681fa5ed (diff) | |
Merge PR #10998: Add missing zify class instances
Ack-by: Zimmi48
Diffstat (limited to 'plugins/micromega/ZifyBool.v')
| -rw-r--r-- | plugins/micromega/ZifyBool.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/plugins/micromega/ZifyBool.v b/plugins/micromega/ZifyBool.v index b94b74097b..4060478363 100644 --- a/plugins/micromega/ZifyBool.v +++ b/plugins/micromega/ZifyBool.v @@ -74,6 +74,14 @@ Definition isZero (z : Z) := Z_of_bool (Z.eqb z 0). Definition isLeZero (x : Z) := Z_of_bool (Z.leb x 0). +Instance Op_isZero : UnOp isZero := + { TUOp := isZero; TUOpInj := ltac: (reflexivity) }. +Add UnOp Op_isZero. + +Instance Op_isLeZero : UnOp isLeZero := + { TUOp := isLeZero; TUOpInj := ltac: (reflexivity) }. +Add UnOp Op_isLeZero. + (* Some intermediate lemma *) Lemma Z_eqb_isZero : forall n m, |