ToLevel class

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

class Lean.ToLevel : Type

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

• toLevel : Lean.Level

  A Level that represents the universe level u.

• univ : Sort u → True

  A hack to avoid the "unused universe parameter" error. We can remove this field pending issue https://github.com/leanprover/lean4/issues/2116

instance Lean.instToLevel : Lean.ToLevel

Equations

• Lean.instToLevel = { toLevel := Lean.Level.zero, univ := Lean.instToLevel.proof_1 }

instance Lean.instToLevel_1 [Lean.ToLevel] : Lean.ToLevel

Equations

• Lean.instToLevel_1 = { toLevel := Lean.toLevel.succ, univ := Lean.instToLevel_1.proof_1 }

def Lean.ToLevel.max [Lean.ToLevel] [Lean.ToLevel] : Lean.ToLevel

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

Equations

• Lean.ToLevel.max = { toLevel := Lean.toLevel.max Lean.toLevel, univ := Lean.ToLevel.max.proof_1 }

def Lean.ToLevel.imax [Lean.ToLevel] [Lean.ToLevel] : Lean.ToLevel

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

Equations

• Lean.ToLevel.imax = { toLevel := Lean.toLevel.imax Lean.toLevel, univ := Lean.ToLevel.imax.proof_1 }