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.

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 α

Instances
    Equations
      Instances For
        instance Lean.instToExprFin {n : Nat} :
        Equations
          Equations
            Equations
              Instances For
                Equations
                  Instances For
                    Equations
                      Instances For
                        Equations
                          Instances For
                            Equations
                              Instances For
                                Equations
                                  Equations
                                    Equations
                                      instance Lean.instToExprProdOfToLevel {α : Type u} {β : Type v} [ToLevel] [ToLevel] [ToExpr α] [ToExpr β] :
                                      ToExpr (α × β)
                                      Equations
                                        Equations
                                          Instances For