Documentation

Lean.ToExpr

class Lean.ToExpr (α : Type u) :

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 []
  • toExpr : αLean.Expr

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

  • toTypeExpr : Lean.Expr

    Expression representing the type α

Instances
    Equations
    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.
    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.
    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.
    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.
    Equations
    Equations
    Equations
    Equations
    Equations
    Equations
    Equations
    • One or more equations did not get rendered due to their size.
    instance Lean.instToExprList {α : Type u_1} [Lean.ToExpr α] :
    Equations
    • One or more equations did not get rendered due to their size.
    instance Lean.instToExprArray {α : Type u_1} [Lean.ToExpr α] :
    Equations
    • One or more equations did not get rendered due to their size.
    instance Lean.instToExprProd {α : Type u_1} {β : Type u_2} [Lean.ToExpr α] [Lean.ToExpr β] :
    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.
    Equations
    Equations
    • One or more equations did not get rendered due to their size.
    Equations
    Instances For