test-suite/output/UnivBinders.out


1
2
3
4
5
6
7
8
9
10
11
12

bar@{u} = nat
     : Wrap@{u} Set
(* u |= Set < u
         *)

bar is universe polymorphic
foo@{u Top.8 v} = 
Type@{Top.8} -> Type@{v} -> Type@{u}
     : Type@{max(u+1, Top.8+1, v+1)}
(* u Top.8 v |=  *)

foo is universe polymorphic