tests/example2.v


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15

Require Import Ltac2.Ltac2.

Ltac2 Notation "split" bnd(bindings) := Std.split bnd.

Goal exists n, n = 0.
Proof.
split with (x := 0).
Std.reflexivity ().
Qed.

Goal exists n, n = 0.
Proof.
split with 0.
split.
Qed.