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)

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 Lean.instToLevel : Lean.ToLevel.{0}

Equations

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

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

Equations

• Lean.instToLevel_1 = { toLevel := Lean.Level.succ Lean.toLevel.{u}, univ := Type u }

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.

Equations

• Lean.ToLevel.max = { toLevel := Lean.Level.max Lean.toLevel.{u} Lean.toLevel.{v}, univ := Sort (max u v) }

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.

Equations

• Lean.ToLevel.imax = { toLevel := Lean.Level.imax Lean.toLevel.{u} Lean.toLevel.{v}, univ := Sort (imax u v) }