ToExpr instances for Auto

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Auto.instToExprProdOfToLevel = { toExpr := Auto.toExprProd✝, toTypeExpr := ((Lean.Expr.const `Prod [Auto.toLevel, Auto.toLevel]).app (Lean.toTypeExpr α✝)).app (Lean.toTypeExpr β✝) }

instance Auto.instToExprFilePath_auto : Lean.ToExpr System.FilePath

Equations

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

instance Auto.instToExprInt_auto : Lean.ToExpr Int

Equations

• Auto.instToExprInt_auto = { toExpr := Auto.toExprInt✝, toTypeExpr := Lean.Expr.const `Int [] }

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

Equations

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

instance Auto.instToExprPUnitOfToLevel [ToLevel] : Lean.ToExpr PUnit

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

Equations

• Auto.instToExprPUnitOfToLevel = { toExpr := fun (x : PUnit) => Lean.mkConst `PUnit.unit [Auto.toLevel], toTypeExpr := Lean.mkConst `PUnit [Auto.toLevel] }

instance Auto.instToExprPos_auto : Lean.ToExpr String.Pos

Equations

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

instance Auto.instToExprSubstring_auto : Lean.ToExpr Substring

Equations

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

instance Auto.instToExprSourceInfo_auto : Lean.ToExpr Lean.SourceInfo

Equations

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

instance Auto.instToExprPreresolved_auto : Lean.ToExpr Lean.Syntax.Preresolved

Equations

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

instance Auto.instToExprSyntax_auto : Lean.ToExpr Lean.Syntax

Equations

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

instance Auto.instToExprMData_auto : Lean.ToExpr Lean.MData

Equations

• Auto.instToExprMData_auto = { toExpr := Auto.toExprMData✝, toTypeExpr := Lean.mkConst `Lean.MData }

instance Auto.instToExprFVarId_auto : Lean.ToExpr Lean.FVarId

Equations

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

instance Auto.instToExprMVarId_auto : Lean.ToExpr Lean.MVarId

Equations

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

instance Auto.instToExprLevelMVarId_auto : Lean.ToExpr Lean.LevelMVarId

Equations

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

instance Auto.instToExprLevel_auto : Lean.ToExpr Lean.Level

Equations

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

instance Auto.instToExprBinderInfo_auto : Lean.ToExpr Lean.BinderInfo

Equations

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

instance Auto.instToExprLiteral_auto : Lean.ToExpr Lean.Literal

Equations

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

instance Auto.instToExprExpr_auto : Lean.ToExpr Lean.Expr

Equations

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