diff options
| author | Frédéric Besson | 2020-06-23 11:48:21 +0200 |
|---|---|---|
| committer | Frédéric Besson | 2020-06-23 11:48:21 +0200 |
| commit | 700918ada1c864c900bdc065d39c4b16d2a47500 (patch) | |
| tree | d407e4884acf73c9451f89eae3693341f6887a22 /test-suite | |
| parent | 34e62d05df4ecd833f87115aa0e986ef7626359e (diff) | |
| parent | 8095d7d14cea6937346b960063d90cbb159612df (diff) | |
Merge PR #12552: Add a pre-hook mechanism for the `zify` tactic
Reviewed-by: fajb
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. |