Documentation

Mathlib.Tactic.ToExpr

`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 α✝) }

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.instToExprRaw_mathlib :

Lean.ToExpr String.Pos.Raw

Equations

Mathlib.instToExprRaw_mathlib = { toExpr := Mathlib.instToExprRaw_mathlib.toExpr, toTypeExpr := Lean.Expr.const `String.Pos.Raw [] }

def Mathlib.instToExprRaw_mathlib.toExpr :

String.Pos.Raw → Lean.Expr

Equations

Mathlib.instToExprRaw_mathlib.toExpr { byteIdx := a } = (Lean.Expr.const `String.Pos.Raw.mk []).app (Lean.toExpr a)

Instances For

instance Mathlib.instToExprSubstring_mathlib :

Lean.ToExpr Substring

Equations

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

def Mathlib.instToExprSubstring_mathlib.toExpr :

Substring → Lean.Expr

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

def Mathlib.instToExprSourceInfo_mathlib.toExpr :

Lean.SourceInfo → Lean.Expr

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

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

partial def Mathlib.instToExprSyntax_mathlib.toExpr :

Lean.Syntax → Lean.Expr

instance Mathlib.instToExprMData_mathlib :

Lean.ToExpr Lean.MData

Equations

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

def Mathlib.instToExprMVarId_mathlib.toExpr :

Lean.MVarId → Lean.Expr

Equations

Mathlib.instToExprMVarId_mathlib.toExpr { name := a } = (Lean.Expr.const `Lean.MVarId.mk []).app (Lean.toExpr a)

Instances For

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

def Mathlib.instToExprLevelMVarId_mathlib.toExpr :

Lean.LevelMVarId → Lean.Expr

Equations

Mathlib.instToExprLevelMVarId_mathlib.toExpr { name := a } = (Lean.Expr.const `Lean.LevelMVarId.mk []).app (Lean.toExpr a)

Instances For

instance Mathlib.instToExprLevel_mathlib :

Lean.ToExpr Lean.Level

Equations

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

def Mathlib.instToExprLevel_mathlib.toExpr :

Lean.Level → Lean.Expr

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

def Mathlib.instToExprBinderInfo_mathlib.toExpr :

Lean.BinderInfo → Lean.Expr

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

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

def Mathlib.instToExprExpr_mathlib.toExpr :

Lean.Expr → 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)

Instances For