blob: ecebaba8127c3e20e1ae19143307403bcc74d3d1 (
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
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
|
Polymorphic Axiom inhabited@{u} : Type@{u} -> Prop.
Polymorphic Axiom unit@{u} : Type@{u}.
Polymorphic Axiom tt@{u} : inhabited unit@{u}.
Polymorphic Hint Resolve tt : the_lemmas.
Set Printing All.
Set Printing Universes.
Goal inhabited unit.
Proof.
eauto with the_lemmas.
Qed.
Universe u.
Axiom f : Type@{u} -> Prop.
Lemma fapp (X : Type) : f X -> False.
Admitted.
Polymorphic Axiom funi@{i} : f unit@{i}.
Goal (forall U, f U) -> (*(f unit -> False) -> *)False /\ False.
eauto using (fapp unit funi). (* The two fapp's have different universes *)
Qed.
Hint Resolve (fapp unit funi) : mylems.
Goal (forall U, f U) -> (*(f unit -> False) -> *)False /\ False.
eauto with mylems. (* Forces the two fapps at the same level *)
Qed.
Goal (forall U, f U) -> (f unit -> False) -> False /\ False.
eauto. (* Forces the two fapps at the same level *)
Qed.
Polymorphic Definition MyType@{i} := Type@{i}.
Universes l m n.
Constraint l < m.
Polymorphic Axiom maketype@{i} : MyType@{i}.
Goal MyType@{l}.
Proof.
Fail solve [ eauto using maketype@{m} ].
eauto using maketype.
Undo.
eauto using maketype@{n}.
Qed.
Axiom foo : forall (A : Type), list A.
Polymorphic Axiom foop@{i} : forall (A : Type@{i}), list A.
Universe x y.
Goal list Type@{x}.
Proof.
eauto using (foo Type). (* Refreshes the term *)
Undo.
eauto using foo. Show Universes.
Undo.
eauto using foop. Show Proof. Show Universes.
Qed.
|
