ToExpr instances for Mathlib

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

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

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

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

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

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

instance Mathlib.instToExprRaw_mathlib_1 : Lean.ToExpr Substring.Raw

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

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

instance Mathlib.instToExprSourceInfo_mathlib : Lean.ToExpr Lean.SourceInfo

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

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

instance Mathlib.instToExprMVarId_mathlib : Lean.ToExpr Lean.MVarId

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

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

instance Mathlib.instToExprExpr_mathlib : Lean.ToExpr Lean.Expr