ToLevel class

This module defines Lean.ToLevel, which is the Lean.Level analogue to Lean.ToExpr.

Warning: Import Mathlib.Tactic.ToExpr instead of this one if you are writing ToExpr instances. This ensures that you are using the universe polymorphic ToExpr instances that override the ones from Lean 4 core.

class Lean.ToLevel : Type (u + 1)

• toLevel : Lean.Level

  A Level that represents the universe level u.

• univ : Type u

  The universe itself. This is only here to avoid the "unused universe parameter" error.

A class to create Level expressions that denote particular universe levels in Lean. Lean.ToLevel.toLevel.{u} evaluates to a Lean.Level term representing u

instance Lean.instToLevel : Lean.ToLevel.{0}

instance Lean.instToLevel_1 [Lean.ToLevel.{u}] : Lean.ToLevel.{u + 1}

def Lean.ToLevel.max [Lean.ToLevel.{u}] [Lean.ToLevel.{v}] : Lean.ToLevel.{max u v}

ToLevel for max u v. This is not an instance since it causes divergence.

def Lean.ToLevel.imax [Lean.ToLevel.{u}] [Lean.ToLevel.{v}] : Lean.ToLevel.{imax u v}

ToLevel for imax u v. This is not an instance since it causes divergence.