diff options
| author | Kazuhiko Sakaguchi | 2020-06-20 20:45:15 +0900 |
|---|---|---|
| committer | Kazuhiko Sakaguchi | 2020-06-20 21:58:49 +0900 |
| commit | 8095d7d14cea6937346b960063d90cbb159612df (patch) | |
| tree | 609ea84add5d5fca94882e104872b2970749fc57 /test-suite | |
| parent | 43dba0d74b6cc39eea149c2908291e9108d21e71 (diff) | |
Add a pre-hook mechanism for the `zify` tactic
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. |