diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/micromega/zify.v | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/test-suite/micromega/zify.v b/test-suite/micromega/zify.v index 8fd7398638..a12623c3c0 100644 --- a/test-suite/micromega/zify.v +++ b/test-suite/micromega/zify.v @@ -159,7 +159,7 @@ Require Import ZifyClasses. Require Import ZifyInst. Instance Zero : CstOp (@zero znat : nat) := Op_O. -Add CstOp Zero. +Add Zify CstOp Zero. Goal @zero znat = 0%nat. @@ -227,3 +227,12 @@ Goal forall (f : Z -> bool), negb (negb (f 0)) = f 0. Proof. intros. lia. Qed. + +Ltac Zify.zify_pre_hook ::= unfold is_true in *. + +Goal forall x y : nat, is_true (Nat.eqb x 1) -> + is_true (Nat.eqb y 0) -> + is_true (Nat.eqb (x + y) 1). +Proof. +lia. +Qed. |