ToExpr instances for Mathlib

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

def Mathlib.instToExprULift_mathlib.toExpr {α✝ : Type s} [Lean.ToExpr α✝] : Lean.ToLevel → Lean.ToLevel → ULift.{r, s} α✝ → Lean.Expr

instance Mathlib.instToExprPUnitOfToLevel_mathlib [Lean.ToLevel] : Lean.ToExpr PUnit.{u + 1}

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

def Mathlib.instToExprRaw_mathlib.toExpr : String.Pos.Raw → Lean.Expr

instance Mathlib.instToExprRaw_mathlib : Lean.ToExpr String.Pos.Raw

def Mathlib.instToExprRaw_mathlib_1.toExpr : Substring.Raw → Lean.Expr

instance Mathlib.instToExprRaw_mathlib_1 : Lean.ToExpr Substring.Raw

instance Mathlib.instToExprSourceInfo_mathlib : Lean.ToExpr Lean.SourceInfo

def Mathlib.instToExprSourceInfo_mathlib.toExpr : Lean.SourceInfo → Lean.Expr

partial def Mathlib.instToExprSyntax_mathlib.toExpr : Lean.Syntax → Lean.Expr

instance Mathlib.instToExprSyntax_mathlib : Lean.ToExpr Lean.Syntax

instance Mathlib.instToExprMData_mathlib : Lean.ToExpr Lean.MData

instance Mathlib.instToExprMVarId_mathlib : Lean.ToExpr Lean.MVarId

def Mathlib.instToExprMVarId_mathlib.toExpr : Lean.MVarId → Lean.Expr

instance Mathlib.instToExprLevelMVarId_mathlib : Lean.ToExpr Lean.LevelMVarId

def Mathlib.instToExprLevelMVarId_mathlib.toExpr : Lean.LevelMVarId → Lean.Expr

instance Mathlib.instToExprLevel_mathlib : Lean.ToExpr Lean.Level

def Mathlib.instToExprLevel_mathlib.toExpr : Lean.Level → Lean.Expr

instance Mathlib.instToExprBinderInfo_mathlib : Lean.ToExpr Lean.BinderInfo

def Mathlib.instToExprBinderInfo_mathlib.toExpr : Lean.BinderInfo → Lean.Expr

instance Mathlib.instToExprExpr_mathlib : Lean.ToExpr Lean.Expr

def Mathlib.instToExprExpr_mathlib.toExpr : Lean.Expr → Lean.Expr