blob: 2c82673edde0c93e35e5df20051d04218f28697d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
Require Import Ltac2.Ltac2.
Goal exists (a: nat), a = 1.
Proof.
match! goal with
| [ |- ?g ] => Control.assert_false (Constr.has_evar g)
end.
eexists.
match! goal with
| [ |- ?g ] => Control.assert_true (Constr.has_evar g)
end.
match! goal with
| [ |- ?x = ?y ] =>
Control.assert_true (Constr.is_evar x);
Control.assert_false (Constr.is_evar y)
end.
Abort.
|
