Documentation

Lean.ToExpr

class Lean.ToExpr (α : Type u) :

Type u

toExpr : α → Lean.Expr
toTypeExpr : Lean.Expr

Instances

instance Lean.instToExprNat:

Lean.ToExpr Nat

Equations

Lean.instToExprNat = { toExpr := Lean.mkNatLit, toTypeExpr := Lean.mkConst `Nat }

instance Lean.instToExprBool:

Lean.ToExpr Bool

Equations

Lean.instToExprBool = { toExpr := fun b => if b = true then Lean.mkConst `Bool.true else Lean.mkConst `Bool.false, toTypeExpr := Lean.mkConst `Bool }

instance Lean.instToExprChar:

Lean.ToExpr Char

Equations

Lean.instToExprChar = { toExpr := fun c => Lean.mkApp (Lean.mkConst `Char.ofNat) (Lean.toExpr (Char.toNat c)), toTypeExpr := Lean.mkConst `Char }

instance Lean.instToExprString:

Lean.ToExpr String

Equations

Lean.instToExprString = { toExpr := Lean.mkStrLit, toTypeExpr := Lean.mkConst `String }

instance Lean.instToExprUnit:

Lean.ToExpr Unit

Equations

Lean.instToExprUnit = { toExpr := fun x => Lean.mkConst `Unit.unit, toTypeExpr := Lean.mkConst `Unit }

def Lean.Name.toExprAux:

Lean.Name → Lean.Expr

Equations

Lean.Name.toExprAux Lean.Name.anonymous = Lean.mkConst `Lean.Name.anonymous
Lean.Name.toExprAux (Lean.Name.str p s a) = Lean.mkAppB (Lean.mkConst `Lean.Name.mkStr) (Lean.Name.toExprAux p) (Lean.toExpr s)
Lean.Name.toExprAux (Lean.Name.num p n a) = Lean.mkAppB (Lean.mkConst `Lean.Name.mkNum) (Lean.Name.toExprAux p) (Lean.toExpr n)

instance Lean.instToExprName:

Lean.ToExpr Lean.Name

Equations

Lean.instToExprName = { toExpr := Lean.Name.toExprAux, toTypeExpr := Lean.mkConst `Lean.Name }

instance Lean.instToExprOption {α : Type} [inst : Lean.ToExpr α] :

Lean.ToExpr (Option α)

Equations

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

def Lean.List.toExprAux {α : Type u_1} [inst : Lean.ToExpr α] (nilFn : Lean.Expr) (consFn : Lean.Expr) :

List α → Lean.Expr

Equations

Lean.List.toExprAux nilFn consFn [] = nilFn
Lean.List.toExprAux nilFn consFn (a :: as) = Lean.mkApp2 consFn (Lean.toExpr a) (Lean.List.toExprAux nilFn consFn as)

instance Lean.instToExprList {α : Type} [inst : Lean.ToExpr α] :

Lean.ToExpr (List α)

Equations

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

instance Lean.instToExprArray {α : Type} [inst : Lean.ToExpr α] :

Lean.ToExpr (Array α)

Equations

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

instance Lean.instToExprProd {α : Type} {β : Type} [inst : Lean.ToExpr α] [inst : Lean.ToExpr β] :

Lean.ToExpr (α × β)

Equations

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