# Documentation

Lean.ToExpr

class Lean.ToExpr (α : Type u) :
• Convert a value a : α into an expression that denotes a

toExpr :
• Expression representing the type α

toTypeExpr : Lean.Expr

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 []

Instances
Equations
Equations
Equations
Equations
Equations
Equations
instance Lean.instToExprOption {α : Type u_1} [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
instance Lean.instToExprList {α : Type u_1} [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
instance Lean.instToExprArray {α : Type u_1} [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
instance Lean.instToExprProd {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] :
Lean.ToExpr (α × β)
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.