ToExpr
instances for Mathlib #
def
Mathlib.instToExprULift_mathlib.toExpr
{α✝ : Type s}
[Lean.ToExpr α✝]
:
Lean.ToLevel → Lean.ToLevel → ULift α✝ → Lean.Expr
Equations
- Mathlib.instToExprULift_mathlib.toExpr inst✝¹ inst✝ { down := a } = ((Lean.Expr.const `ULift.up [Lean.toLevel, Lean.toLevel]).app (Lean.toTypeExpr α✝)).app (Lean.toExpr a)
Instances For
instance
Mathlib.instToExprULift_mathlib
{α✝ : Type s}
[Lean.ToExpr α✝]
[Lean.ToLevel]
[Lean.ToLevel]
:
Lean.ToExpr (ULift α✝)
Equations
- Mathlib.instToExprULift_mathlib = { toExpr := Mathlib.instToExprULift_mathlib.toExpr inst✝¹ inst✝, toTypeExpr := (Lean.Expr.const `ULift [Lean.toLevel, Lean.toLevel]).app (Lean.toTypeExpr α✝) }
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] }
Equations
- Mathlib.instToExprRaw_mathlib = { toExpr := Mathlib.instToExprRaw_mathlib.toExpr, toTypeExpr := Lean.Expr.const `String.Pos.Raw [] }
Equations
- Mathlib.instToExprRaw_mathlib.toExpr { byteIdx := a } = (Lean.Expr.const `String.Pos.Raw.mk []).app (Lean.toExpr a)
Instances For
Equations
- Mathlib.instToExprSubstring_mathlib = { toExpr := Mathlib.instToExprSubstring_mathlib.toExpr, toTypeExpr := Lean.Expr.const `Substring [] }
Equations
- Mathlib.instToExprSubstring_mathlib.toExpr { str := a, startPos := a_1, stopPos := a_2 } = (((Lean.Expr.const `Substring.mk []).app (Lean.toExpr a)).app (Lean.toExpr a_1)).app (Lean.toExpr a_2)
Instances For
Equations
- One or more equations did not get rendered due to their size.
- Mathlib.instToExprSourceInfo_mathlib.toExpr Lean.SourceInfo.none = Lean.Expr.const `Lean.SourceInfo.none []
Instances For
Equations
- Mathlib.instToExprSourceInfo_mathlib = { toExpr := Mathlib.instToExprSourceInfo_mathlib.toExpr, toTypeExpr := Lean.Expr.const `Lean.SourceInfo [] }
Equations
- Mathlib.instToExprSyntax_mathlib = { toExpr := Mathlib.instToExprSyntax_mathlib.toExpr, toTypeExpr := Lean.Expr.const `Lean.Syntax [] }
Equations
- Mathlib.instToExprMData_mathlib = { toExpr := Mathlib.toExprMData✝, toTypeExpr := Lean.mkConst `Lean.MData }
Equations
- Mathlib.instToExprMVarId_mathlib.toExpr { name := a } = (Lean.Expr.const `Lean.MVarId.mk []).app (Lean.toExpr a)
Instances For
Equations
- Mathlib.instToExprMVarId_mathlib = { toExpr := Mathlib.instToExprMVarId_mathlib.toExpr, toTypeExpr := Lean.Expr.const `Lean.MVarId [] }
Equations
- Mathlib.instToExprLevelMVarId_mathlib = { toExpr := Mathlib.instToExprLevelMVarId_mathlib.toExpr, toTypeExpr := Lean.Expr.const `Lean.LevelMVarId [] }
Equations
- Mathlib.instToExprLevelMVarId_mathlib.toExpr { name := a } = (Lean.Expr.const `Lean.LevelMVarId.mk []).app (Lean.toExpr a)
Instances For
Equations
- Mathlib.instToExprLevel_mathlib = { toExpr := Mathlib.instToExprLevel_mathlib.toExpr, toTypeExpr := Lean.Expr.const `Lean.Level [] }
Equations
- Mathlib.instToExprLevel_mathlib.toExpr Lean.Level.zero = Lean.Expr.const `Lean.Level.zero []
- Mathlib.instToExprLevel_mathlib.toExpr a.succ = (Lean.Expr.const `Lean.Level.succ []).app (Mathlib.instToExprLevel_mathlib.toExpr a)
- Mathlib.instToExprLevel_mathlib.toExpr (a.max a_1) = ((Lean.Expr.const `Lean.Level.max []).app (Mathlib.instToExprLevel_mathlib.toExpr a)).app (Mathlib.instToExprLevel_mathlib.toExpr a_1)
- Mathlib.instToExprLevel_mathlib.toExpr (a.imax a_1) = ((Lean.Expr.const `Lean.Level.imax []).app (Mathlib.instToExprLevel_mathlib.toExpr a)).app (Mathlib.instToExprLevel_mathlib.toExpr a_1)
- Mathlib.instToExprLevel_mathlib.toExpr (Lean.Level.param a) = (Lean.Expr.const `Lean.Level.param []).app (Lean.toExpr a)
- Mathlib.instToExprLevel_mathlib.toExpr (Lean.Level.mvar a) = (Lean.Expr.const `Lean.Level.mvar []).app (Lean.toExpr a)
Instances For
Equations
- Mathlib.instToExprBinderInfo_mathlib.toExpr Lean.BinderInfo.default = Lean.Expr.const `Lean.BinderInfo.default []
- Mathlib.instToExprBinderInfo_mathlib.toExpr Lean.BinderInfo.implicit = Lean.Expr.const `Lean.BinderInfo.implicit []
- Mathlib.instToExprBinderInfo_mathlib.toExpr Lean.BinderInfo.strictImplicit = Lean.Expr.const `Lean.BinderInfo.strictImplicit []
- Mathlib.instToExprBinderInfo_mathlib.toExpr Lean.BinderInfo.instImplicit = Lean.Expr.const `Lean.BinderInfo.instImplicit []
Instances For
Equations
- Mathlib.instToExprBinderInfo_mathlib = { toExpr := Mathlib.instToExprBinderInfo_mathlib.toExpr, toTypeExpr := Lean.Expr.const `Lean.BinderInfo [] }
Equations
- Mathlib.instToExprExpr_mathlib = { toExpr := Mathlib.instToExprExpr_mathlib.toExpr, toTypeExpr := Lean.Expr.const `Lean.Expr [] }
Equations
- One or more equations did not get rendered due to their size.
- Mathlib.instToExprExpr_mathlib.toExpr (Lean.Expr.bvar a) = (Lean.Expr.const `Lean.Expr.bvar []).app (Lean.toExpr a)
- Mathlib.instToExprExpr_mathlib.toExpr (Lean.Expr.fvar a) = (Lean.Expr.const `Lean.Expr.fvar []).app (Lean.toExpr a)
- Mathlib.instToExprExpr_mathlib.toExpr (Lean.Expr.mvar a) = (Lean.Expr.const `Lean.Expr.mvar []).app (Lean.toExpr a)
- Mathlib.instToExprExpr_mathlib.toExpr (Lean.Expr.sort a) = (Lean.Expr.const `Lean.Expr.sort []).app (Lean.toExpr a)
- Mathlib.instToExprExpr_mathlib.toExpr (Lean.Expr.const a a_1) = ((Lean.Expr.const `Lean.Expr.const []).app (Lean.toExpr a)).app (Lean.toExpr a_1)
- Mathlib.instToExprExpr_mathlib.toExpr (a.app a_1) = ((Lean.Expr.const `Lean.Expr.app []).app (Mathlib.instToExprExpr_mathlib.toExpr a)).app (Mathlib.instToExprExpr_mathlib.toExpr a_1)
- Mathlib.instToExprExpr_mathlib.toExpr (Lean.Expr.lit a) = (Lean.Expr.const `Lean.Expr.lit []).app (Lean.toExpr a)
- Mathlib.instToExprExpr_mathlib.toExpr (Lean.Expr.mdata a a_1) = ((Lean.Expr.const `Lean.Expr.mdata []).app (Lean.toExpr a)).app (Mathlib.instToExprExpr_mathlib.toExpr a_1)