9 lines
180 B
Text
9 lines
180 B
Text
universe u v w
|
|
|
|
set_option pp.universes true
|
|
#check Type (max u v w)
|
|
#check Type u
|
|
#check @id.{max u v w}
|
|
#check Monad.{max u v, w+1}
|
|
#check Type (max (u+1) w (v+2))
|
|
#check Type _
|