2013-09-02 19:24:29 +00:00
|
|
|
Variable x : Type max U+1+2 M+1 M+2 3
|
2013-08-19 01:37:47 +00:00
|
|
|
Check x
|
2013-09-02 19:24:29 +00:00
|
|
|
Variable f : Type U+10 -> Type
|
2013-08-19 01:37:47 +00:00
|
|
|
Check f
|
|
|
|
|
Check f x
|
|
|
|
|
Check Type 4
|
|
|
|
|
Check x
|
2013-09-02 19:24:29 +00:00
|
|
|
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
|
