Documentation

Lean.ToLevel

ToLevel class #

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

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

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

          Equations
            Instances For