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

• toExpr : α → Lean.Expr

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

• toTypeExpr : Lean.Expr

  Expression representing the type α

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

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

instance Lean.instToExprNat : Lean.ToExpr Nat

instance Lean.instToExprBool : Lean.ToExpr Bool

instance Lean.instToExprChar : Lean.ToExpr Char

instance Lean.instToExprString : Lean.ToExpr String

instance Lean.instToExprUnit : Lean.ToExpr Unit

instance Lean.instToExprName : Lean.ToExpr Lake.Name

instance Lean.instToExprOption {α : Type u_1} [Lean.ToExpr α] : Lean.ToExpr (Option α)

instance Lean.instToExprList {α : Type u_1} [Lean.ToExpr α] : Lean.ToExpr (List α)

instance Lean.instToExprArray {α : Type u_1} [Lean.ToExpr α] : Lean.ToExpr (Array α)

instance Lean.instToExprProd {α : Type u_1} {β : Type u_2} [Lean.ToExpr α] [Lean.ToExpr β] : Lean.ToExpr (α × β)

def Lean.Expr.toCtorIfLit : Lean.Expr → Lean.Expr