aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/simpl.v
blob: 5f1926f1420b1155b7350d2d0de11b8aae4d542c (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
(* Simpl with patterns *)

Goal forall x, 0+x = 1+x.
intro x.
simpl (_ + x).
Show.
Undo.
simpl (_ + x) at 2.
Show.
Undo.
simpl (0 + _).
Show.
Undo.