Lean.ToExpr

source

class Lean.ToExpr (α : Type u) :

Type u

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

Instances

source

instance Lean.instToExprNat :

Lean.ToExpr Nat

Equations

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

source

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 }

source

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 }

source

instance Lean.instToExprString :

Lean.ToExpr String

Equations

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

source

instance Lean.instToExprUnit :

Lean.ToExpr Unit

Equations

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

source

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 x_1) = Lean.mkAppB (Lean.mkConst `Lean.Name.mkStr) (Lean.Name.toExprAux p) (Lean.toExpr s)
Lean.Name.toExprAux (Lean.Name.num p n x_1) = Lean.mkAppB (Lean.mkConst `Lean.Name.mkNum) (Lean.Name.toExprAux p) (Lean.toExpr n)

source

instance Lean.instToExprName :

Lean.ToExpr Lean.Name

Equations

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

source

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

Lean.ToExpr (Option α)

Equations

Lean.instToExprOption = let type := Lean.toTypeExpr α; { toExpr := fun o => match o with | none => Lean.mkApp (Lean.mkConst `Option.none [Lean.levelZero]) type | some a => Lean.mkApp2 (Lean.mkConst `Option.some [Lean.levelZero]) type (Lean.toExpr a), toTypeExpr := Lean.mkApp (Lean.mkConst `Option [Lean.levelZero]) type }

source

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)

source

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

Lean.ToExpr (List α)

Equations

Lean.instToExprList = let type := Lean.toTypeExpr α; let nil := Lean.mkApp (Lean.mkConst `List.nil [Lean.levelZero]) type; let cons := Lean.mkApp (Lean.mkConst `List.cons [Lean.levelZero]) type; { toExpr := Lean.List.toExprAux nil cons, toTypeExpr := Lean.mkApp (Lean.mkConst `List [Lean.levelZero]) type }

source

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

Lean.ToExpr (Array α)

Equations

Lean.instToExprArray = let type := Lean.toTypeExpr α; { toExpr := fun as => Lean.mkApp2 (Lean.mkConst `List.toArray [Lean.levelZero]) type (Lean.toExpr (Array.toList as)), toTypeExpr := Lean.mkApp (Lean.mkConst `Array [Lean.levelZero]) type }

source

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

Lean.ToExpr (α × β)

Equations

Lean.instToExprProd = let αType := Lean.toTypeExpr α; let βType := Lean.toTypeExpr β; { toExpr := fun x => match x with | (a, b) => Lean.mkApp4 (Lean.mkConst `Prod.mk [Lean.levelZero, Lean.levelZero]) αType βType (Lean.toExpr a) (Lean.toExpr b), toTypeExpr := Lean.mkApp2 (Lean.mkConst `Prod [Lean.levelZero, Lean.levelZero]) αType βType }