Lean.ToExpr

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 : α → Lean.Expr
Convert a value a : α into an expression that denotes a
toTypeExpr : Lean.Expr
Expression representing the type α

Instances

source

instance Lean.instToExprNat :

Lean.ToExpr Nat

Equations

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

source

instance Lean.instToExprInt :

Lean.ToExpr Int

Equations

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

source

def Lean.instToExprInt.mkNat (n : Nat) :

Lean.Expr

Equations

Lean.instToExprInt.mkNat n = Lean.mkApp3 (Lean.Expr.const `OfNat.ofNat [0]) (Lean.Expr.const `Int []) (Lean.mkRawNatLit n) ((Lean.Expr.const `instOfNat []).app (Lean.mkRawNatLit n))

Instances For

source

instance Lean.instToExprFin {n : Nat} :

Lean.ToExpr (Fin n)

Equations

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

source

instance Lean.instToExprBitVec {n : Nat} :

Lean.ToExpr (BitVec n)

Equations

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

source

instance Lean.instToExprUInt8 :

Lean.ToExpr UInt8

Equations

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

source

instance Lean.instToExprUInt16 :

Lean.ToExpr UInt16

Equations

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

source

instance Lean.instToExprUInt32 :

Lean.ToExpr UInt32

Equations

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

source

instance Lean.instToExprUInt64 :

Lean.ToExpr UInt64

Equations

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

source

instance Lean.instToExprUSize :

Lean.ToExpr USize

Equations

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

source

instance Lean.instToExprBool :

Lean.ToExpr Bool

Equations

Lean.instToExprBool = { toExpr := fun (b : Bool) => 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 : Char) => Lean.mkApp (Lean.mkConst `Char.ofNat) (Lean.mkRawNatLit c.toNat), 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 : Unit) => Lean.mkConst `Unit.unit, toTypeExpr := Lean.mkConst `Unit }

source

instance Lean.instToExprFilePath :

Lean.ToExpr System.FilePath

Equations

Lean.instToExprFilePath = { toExpr := fun (p : System.FilePath) => Lean.mkApp (Lean.mkConst `System.FilePath.mk) (Lean.toExpr p.toString), toTypeExpr := Lean.mkConst `System.FilePath }

source

instance Lean.instToExprName :

Lean.ToExpr Lean.Name

Equations

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

source

instance Lean.instToExprOptionOfToLevel {α : Type u} [Lean.ToLevel] [Lean.ToExpr α] :

Lean.ToExpr (Option α)

Equations

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

source

instance Lean.instToExprListOfToLevel {α : Type u} [Lean.ToLevel] [Lean.ToExpr α] :

Lean.ToExpr (List α)

Equations

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

source

instance Lean.instToExprArrayOfToLevel {α : Type u} [Lean.ToLevel] [Lean.ToExpr α] :

Lean.ToExpr (Array α)

Equations

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

source

instance Lean.instToExprProdOfToLevel {α : Type u} {β : Type v} [Lean.ToLevel] [Lean.ToLevel] [Lean.ToExpr α] [Lean.ToExpr β] :

Lean.ToExpr (α × β)

Equations

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

source

instance Lean.instToExprLiteral :

Lean.ToExpr Lean.Literal

Equations

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

source

instance Lean.instToExprFVarId :

Lean.ToExpr Lean.FVarId

Equations

Lean.instToExprFVarId = { toExpr := fun (fvarId : Lean.FVarId) => Lean.mkApp (Lean.mkConst `Lean.FVarId.mk) (Lean.toExpr fvarId.name), toTypeExpr := Lean.mkConst `Lean.FVarId }

source

instance Lean.instToExprPreresolved :

Lean.ToExpr Lean.Syntax.Preresolved

Equations

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

source

def Lean.Expr.toCtorIfLit :

Lean.Expr → Lean.Expr

Equations

(Lean.Expr.lit (Lean.Literal.natVal v)).toCtorIfLit = if (v == 0) = true then Lean.mkConst `Nat.zero else Lean.mkApp (Lean.mkConst `Nat.succ) (Lean.mkRawNatLit (v - 1))
(Lean.Expr.lit (Lean.Literal.strVal v)).toCtorIfLit = Lean.mkApp (Lean.mkConst `String.mk) (Lean.toExpr v.toList)
x✝.toCtorIfLit = x✝

Instances For