blob: 1eb84a9bef2e15a5bce3fbf657e9f1dd44a63a9b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
(* Refine and let-in's *)
Goal (EX x:nat | x=O).
Refine let y = (plus O O) in ?.
Exists y; Auto.
Save test1.
Goal (EX x:nat | x=O).
Refine let y = (plus O O) in (ex_intro ? ? (plus y y) ?).
Auto.
Save test2.
Goal nat.
Refine let y = O in (plus O ?).
Exact (S O).
Save test3.
|
