blob: 398f33561e48e006b970035aefa60271e4ca6dc1 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
Require Import Ltac2.Ltac2.
Import Ltac2.Notations.
Goal exists n, n = 0.
Proof.
split with (x := 0).
Std.reflexivity ().
Qed.
Goal exists n, n = 0.
Proof.
split with 0.
split.
Qed.
Goal exists n, n = 0.
Proof.
let myvar := Std.NamedHyp @x in split with (?myvar := 0).
split.
Qed.
|
