aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/set.v
blob: 0e745354ab3a1a664e3eb913e91a222a08053612 (plain)
1
2
3
4
5
6
7
8
9
10
Goal let x:=O+O in x=x.
intro.
set (y1:=O) in (type of x).
Show.
set (y2:=O) in (value of x) at 1.
Show.
set (y3:=O) in (value of x).
Show.
trivial.
Qed.