Documentation

Mathlib.Tactic.ToExpr

ToExpr instances for Mathlib #

This module should be imported by any module that intends to define ToExpr instances. It provides necessary dependencies (the Lean.ToLevel class) and it also overrides the instances that come from core Lean 4 that do not handle universe polymorphism. (See the module Lean.ToExpr for the instances that are overridden.)

In addition, we provide some additional ToExpr instances for core definitions.

instance Lean.instToExprOptionOfToLevel :
{α : Type u} → [inst : Lean.ToExpr α] → [inst : Lean.ToLevel.{u}] → Lean.ToExpr (Option α)
Equations
  • Lean.instToExprOptionOfToLevel = { toExpr := Lean.toExprOption✝, toTypeExpr := (Lean.Expr.const `Option [Lean.toLevel.{?u.24}]).app (Lean.toTypeExpr α) }
instance Lean.instToExprListOfToLevel :
{α : Type u} → [inst : Lean.ToExpr α] → [inst : Lean.ToLevel.{u}] → Lean.ToExpr (List α)
Equations
Equations
  • One or more equations did not get rendered due to their size.
instance Lean.instToExprProdOfToLevel :
{α : Type u} → {β : Type v} → [inst : Lean.ToExpr α] → [inst : Lean.ToExpr β] → [inst : Lean.ToLevel.{u}] → [inst : Lean.ToLevel.{v}] → Lean.ToExpr (α × β)
Equations
  • One or more equations did not get rendered due to their size.
instance Mathlib.instToExprULiftOfToLevel :
{α : Type s} → [inst : Lean.ToExpr α] → [inst : Lean.ToLevel.{r}] → [inst : Lean.ToLevel.{s}] → Lean.ToExpr (ULift α)
Equations
  • Mathlib.instToExprULiftOfToLevel = { toExpr := Mathlib.toExprULift✝, toTypeExpr := (Lean.Expr.const `ULift [Lean.toLevel.{?u.31}, Lean.toLevel.{?u.30}]).app (Lean.toTypeExpr α) }

Hand-written instance since PUnit is a Sort rather than a Type.

Equations
  • Mathlib.instToExprPUnitOfToLevel = { toExpr := fun (x : PUnit) => Lean.mkConst `PUnit.unit [Lean.toLevel.{?u.12 + 1}], toTypeExpr := Lean.mkConst `PUnit [Lean.toLevel.{?u.12 + 1}] }