blob: 7f6f9d6279053a6f838d544b42ac003fcef2e55a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
|
Axiom T : Type.
Lemma foo : True * Type.
Proof.
split.
par: abstract (exact I || exact T).
Defined.
(* Yes, these names are generated hence
the test is fragile. I want to assert
that abstract was correctly handled
by par: *)
Check foo_subproof.
Check foo_subproof0.
Check (refl_equal _ :
foo =
pair foo_subproof foo_subproof0).
Lemma bar : True * Type.
Proof.
split.
par: (exact I || exact T).
Defined.
Check (refl_equal _ :
bar = pair I T).
|
