class Lean.ToExpr (α : 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.instToExprProd {α : Type u_1} {β : Type u_2} [Lean.ToExpr α] [Lean.ToExpr β] :
    Lean.ToExpr (α × β)