Documentation

Mathlib.Tactic.ToExpr

`ToExpr` instances for Mathlib #

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

Lean.ToExpr (ULift α✝)

Equations

Mathlib.instToExprULiftOfToLevel_mathlib = { toExpr := Mathlib.toExprULift✝ 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.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.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.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.instToExprExpr_mathlib :

Lean.ToExpr Lean.Expr

Equations

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