Documentation

Mathlib.Tactic.ToLevel

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

Instances
    Equations

    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) }
    Instances For

      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) }
      Instances For