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

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

  toExpr : α → Lean.Expr

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

instance Lean.instToExprNat : Lean.ToExpr Nat

Equations

• Lean.instToExprNat = { toExpr := Lean.mkNatLit, toTypeExpr := Lean.mkConst (Lean.Name.mkStr1 "Nat") }

instance Lean.instToExprBool : Lean.ToExpr Bool

Equations

• One or more equations did not get rendered due to their size.

instance Lean.instToExprChar : Lean.ToExpr Char

Equations

• One or more equations did not get rendered due to their size.

instance Lean.instToExprString : Lean.ToExpr String

Equations

• Lean.instToExprString = { toExpr := Lean.mkStrLit, toTypeExpr := Lean.mkConst (Lean.Name.mkStr1 "String") }

instance Lean.instToExprUnit : Lean.ToExpr Unit

Equations

• Lean.instToExprUnit = { toExpr := fun x => Lean.mkConst (Lean.Name.mkStr2 "Unit" "unit"), toTypeExpr := Lean.mkConst (Lean.Name.mkStr1 "Unit") }

instance Lean.instToExprName : Lean.ToExpr Lean.Name

Equations

• Lean.instToExprName = { toExpr := Lean.Name.toExprAux, toTypeExpr := Lean.mkConst (Lean.Name.mkStr2 "Lean" "Name") }

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.