ToExpr instances for Mathlib

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

Equations

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

instance Mathlib.instToExprPUnitOfToLevel_mathlib [Lean.ToLevel] : Lean.ToExpr PUnit

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

Equations

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

instance Mathlib.instToExprPos_mathlib : Lean.ToExpr String.Pos

Equations

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

instance Mathlib.instToExprSubstring_mathlib : Lean.ToExpr Substring

Equations

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

instance Mathlib.instToExprSourceInfo_mathlib : Lean.ToExpr Lean.SourceInfo

Equations

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

instance Mathlib.instToExprSyntax_mathlib : Lean.ToExpr Lean.Syntax

Equations

• Mathlib.instToExprSyntax_mathlib = { toExpr := Mathlib.instToExprSyntax_mathlib.toExpr✝, 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.instToExprMVarId_mathlib : Lean.ToExpr Lean.MVarId

Equations

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

instance Mathlib.instToExprLevelMVarId_mathlib : Lean.ToExpr Lean.LevelMVarId

Equations

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

instance Mathlib.instToExprLevel_mathlib : Lean.ToExpr Lean.Level

Equations

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

instance Mathlib.instToExprBinderInfo_mathlib : Lean.ToExpr Lean.BinderInfo

Equations

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

instance Mathlib.instToExprExpr_mathlib : Lean.ToExpr Lean.Expr

Equations

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