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} [Lean.ToExpr α✝] [Lean.ToLevel.{u}] : Lean.ToExpr (Option α✝)

Equations

• Lean.instToExprOptionOfToLevel = { toExpr := Lean.toExprOption✝, toTypeExpr := (Lean.Expr.const `Option [Lean.toLevel.{?u.22}]).app (Lean.toTypeExpr α✝) }

instance Lean.instToExprListOfToLevel {α✝ : Type u} [Lean.ToExpr α✝] [Lean.ToLevel.{u}] : Lean.ToExpr (List α✝)

Equations

• Lean.instToExprListOfToLevel = { toExpr := Lean.toExprList✝, toTypeExpr := (Lean.Expr.const `List [Lean.toLevel.{?u.22}]).app (Lean.toTypeExpr α✝) }

instance Lean.instToExprArrayOfToLevel {α : Type u} [Lean.ToExpr α] [Lean.ToLevel.{u}] : Lean.ToExpr (Array α)

Equations

• One or more equations did not get rendered due to their size.

instance Lean.instToExprProdOfToLevel {α✝ : Type u} {β✝ : Type v} [Lean.ToExpr α✝] [Lean.ToExpr β✝] [Lean.ToLevel.{u}] [Lean.ToLevel.{v}] : Lean.ToExpr (α✝ × β✝)

Equations

• One or more equations did not get rendered due to their size.

instance Lean.instToExprFilePath_mathlib : Lean.ToExpr System.FilePath

Equations

• Lean.instToExprFilePath_mathlib = { toExpr := Lean.toExprFilePath✝, toTypeExpr := Lean.Expr.const `System.FilePath [] }

instance Mathlib.instToExprULiftOfToLevel {α✝ : Type s} [Lean.ToExpr α✝] [Lean.ToLevel.{r}] [Lean.ToLevel.{s}] : Lean.ToExpr (ULift α✝)

Equations

• Mathlib.instToExprULiftOfToLevel = { toExpr := Mathlib.toExprULift✝, toTypeExpr := (Lean.Expr.const `ULift [Lean.toLevel.{?u.28}, Lean.toLevel.{?u.27}]).app (Lean.toTypeExpr α✝) }

instance Mathlib.instToExprPUnitOfToLevel [Lean.ToLevel.{u}] : Lean.ToExpr PUnit

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}] }

instance Mathlib.instToExprPos_mathlib : Lean.ToExpr String.Pos

Equations

• Mathlib.instToExprPos_mathlib = { toExpr := Mathlib.toExprPos✝, toTypeExpr := Lean.Expr.const `String.Pos [] }

instance Mathlib.instToExprSubstring_mathlib : Lean.ToExpr Substring

Equations

• Mathlib.instToExprSubstring_mathlib = { toExpr := Mathlib.toExprSubstring✝, toTypeExpr := Lean.Expr.const `Substring [] }

instance Mathlib.instToExprSourceInfo_mathlib : Lean.ToExpr Lean.SourceInfo

Equations

• Mathlib.instToExprSourceInfo_mathlib = { toExpr := Mathlib.toExprSourceInfo✝, toTypeExpr := Lean.Expr.const `Lean.SourceInfo [] }

instance Mathlib.instToExprPreresolved_mathlib : Lean.ToExpr Lean.Syntax.Preresolved

Equations

• Mathlib.instToExprPreresolved_mathlib = { toExpr := Mathlib.toExprPreresolved✝, toTypeExpr := Lean.Expr.const `Lean.Syntax.Preresolved [] }

instance Mathlib.instToExprSyntax_mathlib : Lean.ToExpr Lean.Syntax

Equations

• Mathlib.instToExprSyntax_mathlib = { toExpr := Mathlib.toExprSyntax✝, toTypeExpr := Lean.Expr.const `Lean.Syntax [] }

instance Mathlib.instToExprMData_mathlib : Lean.ToExpr Lean.MData

Equations

• Mathlib.instToExprMData_mathlib = { toExpr := Mathlib.toExprMData✝, toTypeExpr := Lean.mkConst `Lean.MData }

instance Mathlib.instToExprFVarId_mathlib : Lean.ToExpr Lean.FVarId

Equations

• Mathlib.instToExprFVarId_mathlib = { toExpr := Mathlib.toExprFVarId✝, toTypeExpr := Lean.Expr.const `Lean.FVarId [] }

instance Mathlib.instToExprMVarId_mathlib : Lean.ToExpr Lean.MVarId

Equations

• Mathlib.instToExprMVarId_mathlib = { toExpr := Mathlib.toExprMVarId✝, toTypeExpr := Lean.Expr.const `Lean.MVarId [] }

instance Mathlib.instToExprLevelMVarId_mathlib : Lean.ToExpr Lean.LevelMVarId

Equations

• Mathlib.instToExprLevelMVarId_mathlib = { toExpr := Mathlib.toExprLevelMVarId✝, toTypeExpr := Lean.Expr.const `Lean.LevelMVarId [] }

instance Mathlib.instToExprLevel_mathlib : Lean.ToExpr Lean.Level

Equations

• Mathlib.instToExprLevel_mathlib = { toExpr := Mathlib.toExprLevel✝, toTypeExpr := Lean.Expr.const `Lean.Level [] }

instance Mathlib.instToExprBinderInfo_mathlib : Lean.ToExpr Lean.BinderInfo

Equations

• Mathlib.instToExprBinderInfo_mathlib = { toExpr := Mathlib.toExprBinderInfo✝, toTypeExpr := Lean.Expr.const `Lean.BinderInfo [] }

instance Mathlib.instToExprLiteral_mathlib : Lean.ToExpr Lean.Literal

Equations

• Mathlib.instToExprLiteral_mathlib = { toExpr := Mathlib.toExprLiteral✝, toTypeExpr := Lean.Expr.const `Lean.Literal [] }

instance Mathlib.instToExprExpr_mathlib : Lean.ToExpr Lean.Expr

Equations

• Mathlib.instToExprExpr_mathlib = { toExpr := Mathlib.toExprExpr✝, toTypeExpr := Lean.Expr.const `Lean.Expr [] }