class Lean.ToExpr (α : Type u) : Type u

We use the ToExpr type class to convert values of type α into expressions that denote these values in Lean.

Examples:

toExpr true = .const ``Bool.true []

toTypeExpr Bool = .const ``Bool []

See also ToLevel for representing universe levels as Level expressions.

• toExpr : α → Expr

  Convert a value a : α into an expression that denotes a

• toTypeExpr : Expr

  Expression representing the type α

instance Lean.instToExprNat : ToExpr Nat

instance Lean.instToExprInt : ToExpr Int

def Lean.instToExprInt.mkNat (n : Nat) : Expr

instance Lean.instToExprFin {n : Nat} : ToExpr (Fin n)

instance Lean.instToExprBitVec {n : Nat} : ToExpr (BitVec n)

instance Lean.instToExprUInt8 : ToExpr UInt8

instance Lean.instToExprUInt16 : ToExpr UInt16

instance Lean.instToExprUInt32 : ToExpr UInt32

instance Lean.instToExprUInt64 : ToExpr UInt64

instance Lean.instToExprUSize : ToExpr USize

instance Lean.instToExprInt8 : ToExpr Int8

def Lean.instToExprInt8.mkNat (n : Nat) : Expr

instance Lean.instToExprInt16 : ToExpr Int16

def Lean.instToExprInt16.mkNat (n : Nat) : Expr

instance Lean.instToExprInt32 : ToExpr Int32

def Lean.instToExprInt32.mkNat (n : Nat) : Expr

instance Lean.instToExprInt64 : ToExpr Int64

def Lean.instToExprInt64.mkNat (n : Nat) : Expr

instance Lean.instToExprISize : ToExpr ISize

def Lean.instToExprISize.mkNat (n : Nat) : Expr

instance Lean.instToExprBool : ToExpr Bool

instance Lean.instToExprChar : ToExpr Char

instance Lean.instToExprString : ToExpr String

instance Lean.instToExprUnit : ToExpr Unit

instance Lean.instToExprFilePath : ToExpr System.FilePath

instance Lean.instToExprName : ToExpr Name

instance Lean.instToExprOptionOfToLevel {α : Type u} [ToLevel] [ToExpr α] : ToExpr (Option α)

instance Lean.instToExprListOfToLevel {α : Type u} [ToLevel] [ToExpr α] : ToExpr (List α)

instance Lean.instToExprArrayOfToLevel {α : Type u} [ToLevel] [ToExpr α] : ToExpr (Array α)

instance Lean.instToExprProdOfToLevel {α : Type u} {β : Type v} [ToLevel] [ToLevel] [ToExpr α] [ToExpr β] : ToExpr (α × β)

instance Lean.instToExprLiteral : ToExpr Literal

instance Lean.instToExprFVarId : ToExpr FVarId

instance Lean.instToExprPreresolved : ToExpr Syntax.Preresolved

def Lean.Expr.toCtorIfLit : Expr → Expr