20 lines
426 B
Text
20 lines
426 B
Text
Variable x : Type max U+1+2 M+1 M+2 3
|
|
Check x
|
|
Variable f : Type U+10 -> Type
|
|
Check f
|
|
Check f x
|
|
Check Type 4
|
|
Check x
|
|
Check Type max U M
|
|
Show Type U+3
|
|
Check Type U+3
|
|
Check Type U ⊔ M
|
|
Check Type U ⊔ M ⊔ 3
|
|
Show Type U+1 ⊔ M ⊔ 3
|
|
Check Type U+1 ⊔ M ⊔ 3
|
|
Show Type U -> Type 5
|
|
Check Type U -> Type 5
|
|
Check Type M ⊔ 3 -> Type U+5
|
|
Show Type M ⊔ 3 -> Type U -> Type 5
|
|
Check Type M ⊔ 3 -> Type U -> Type 5
|
|
Show Type U
|