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 : 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 : ToLevel

Equations

• Lean.instToLevel = { toLevel := Lean.Level.zero }

instance Lean.instToLevel_1 [ToLevel] : ToLevel

Equations

• Lean.instToLevel_1 = { toLevel := Lean.toLevel.succ }

def Lean.ToLevel.max [ToLevel] [ToLevel] : 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 }

def Lean.ToLevel.imax [ToLevel] [ToLevel] : 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 }