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 Auto.ToLevel : Type (u + 1)

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 : Type u

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

instance Auto.instToLevel : ToLevel

Equations

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

instance Auto.instToLevel_1 [ToLevel] : ToLevel

Equations

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

def Auto.ToLevel.max [ToLevel] [ToLevel] : ToLevel

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

Equations

• Auto.ToLevel.max = { toLevel := Auto.toLevel.max Auto.toLevel }

def Auto.ToLevel.imax [ToLevel] [ToLevel] : ToLevel

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

Equations

• Auto.ToLevel.imax = { toLevel := Auto.toLevel.imax Auto.toLevel }