tests/lean/pplevel.lean - third_party/github.com/leanprover/lean4 - Git at Google


            
            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 _
	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 _