blob: 1bacb751349ac27b0f662835c66f49d9ba0c2dee (
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
|
NonCumulative Inductive Empty@{u} : Type@{u} :=
NonCumulative Record PWrap (A : Type@{u}) : Type@{u} := pwrap { punwrap : A }
PWrap has primitive projections with eta conversion.
For PWrap: Argument scope is [type_scope]
For pwrap: Argument scopes are [type_scope _]
punwrap@{u} =
fun (A : Type@{u}) (p : PWrap@{u} A) => punwrap _ p
: forall A : Type@{u}, PWrap@{u} A -> A
(* u |= *)
punwrap is universe polymorphic
Argument scopes are [type_scope _]
NonCumulative Record RWrap (A : Type@{u}) : Type@{u} := rwrap { runwrap : A }
For RWrap: Argument scope is [type_scope]
For rwrap: Argument scopes are [type_scope _]
runwrap@{u} =
fun (A : Type@{u}) (r : RWrap@{u} A) => let (runwrap) := r in runwrap
: forall A : Type@{u}, RWrap@{u} A -> A
(* u |= *)
runwrap is universe polymorphic
Argument scopes are [type_scope _]
Wrap@{u} = fun A : Type@{u} => A
: Type@{u} -> Type@{u}
(* u |= *)
Wrap is universe polymorphic
Argument scope is [type_scope]
wrap@{u} =
fun (A : Type@{u}) (Wrap : Wrap@{u} A) => Wrap
: forall A : Type@{u}, Wrap@{u} A -> A
(* u |= *)
wrap is universe polymorphic
Arguments A, Wrap are implicit and maximally inserted
Argument scopes are [type_scope _]
bar@{u} = nat
: Wrap@{u} Set
(* u |= Set < u
*)
bar is universe polymorphic
foo@{u Top.17 v} =
Type@{Top.17} -> Type@{v} -> Type@{u}
: Type@{max(u+1, Top.17+1, v+1)}
(* u Top.17 v |= *)
foo is universe polymorphic
Monomorphic mono = Type@{u}
: Type@{u+1}
(* u |= *)
mono is not universe polymorphic
|
