class Lean.ToExpr (α : Type u) : 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

• Lake.instToExprSemVerCore
• Lake.instToExprStdVer
• Lean.Elab.Tactic.BVDecide.Frontend.instToExprBVBinOp
• Lean.Elab.Tactic.BVDecide.Frontend.instToExprBVBinPred
• Lean.Elab.Tactic.BVDecide.Frontend.instToExprBVExpr
• Lean.Elab.Tactic.BVDecide.Frontend.instToExprBVPred
• Lean.Elab.Tactic.BVDecide.Frontend.instToExprBVUnOp
• Lean.Elab.Tactic.BVDecide.Frontend.instToExprBoolExpr
• Lean.Elab.Tactic.BVDecide.Frontend.instToExprGate
• Lean.Elab.Tactic.BVDecide.Frontend.instToExprIntAction
• Lean.Elab.Tactic.Omega.instToExprConstraint
• Lean.Elab.Tactic.Omega.instToExprLinearCombo
• Lean.Meta.DiscrTree.instToExprKey
• Lean.Meta.Simp.Arith.Int.instToExprExpr
• Lean.Meta.Simp.Arith.Int.instToExprPoly
• Lean.Meta.Simp.Arith.Nat.instToExprLinearCnstr
• Lean.Meta.Simp.Arith.Nat.instToExprLinearExpr
• Lean.Meta.instToExprCoeFnInfo
• Lean.Meta.instToExprCoeFnType
• Lean.Position.instToExpr
• Lean.instToExprArrayOfToLevel
• Lean.instToExprBitVec
• Lean.instToExprBool
• Lean.instToExprChar
• Lean.instToExprDeclarationRange
• Lean.instToExprDeclarationRanges
• Lean.instToExprFVarId
• Lean.instToExprFilePath
• Lean.instToExprFin
• Lean.instToExprISize
• Lean.instToExprInt
• Lean.instToExprInt16
• Lean.instToExprInt32
• Lean.instToExprInt64
• Lean.instToExprInt8
• Lean.instToExprListOfToLevel
• Lean.instToExprLiteral
• Lean.instToExprName
• Lean.instToExprNat
• Lean.instToExprOptionOfToLevel
• Lean.instToExprPreresolved
• Lean.instToExprProdOfToLevel
• Lean.instToExprRArray
• Lean.instToExprString
• Lean.instToExprUInt16
• Lean.instToExprUInt32
• Lean.instToExprUInt64
• Lean.instToExprUInt8
• Lean.instToExprUSize
• Lean.instToExprUnit

instance Lean.instToExprNat : ToExpr Nat

Equations

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

instance Lean.instToExprInt : ToExpr Int

Equations

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

def Lean.instToExprInt.mkNat (n : Nat) : 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))

instance Lean.instToExprFin {n : Nat} : ToExpr (Fin n)

Equations

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

instance Lean.instToExprBitVec {n : Nat} : ToExpr (BitVec n)

Equations

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

instance Lean.instToExprUInt8 : ToExpr UInt8

Equations

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

instance Lean.instToExprUInt16 : ToExpr UInt16

Equations

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

instance Lean.instToExprUInt32 : ToExpr UInt32

Equations

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

instance Lean.instToExprUInt64 : ToExpr UInt64

Equations

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

instance Lean.instToExprUSize : ToExpr USize

Equations

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

instance Lean.instToExprInt8 : ToExpr Int8

Equations

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

def Lean.instToExprInt8.mkNat (n : Nat) : Expr

Equations

• Lean.instToExprInt8.mkNat n = Lean.mkApp3 (Lean.Expr.const `OfNat.ofNat [0]) (Lean.Expr.const `Int8 []) (Lean.mkRawNatLit n) ((Lean.Expr.const `Int8.instOfNat []).app (Lean.mkRawNatLit n))

instance Lean.instToExprInt16 : ToExpr Int16

Equations

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

def Lean.instToExprInt16.mkNat (n : Nat) : Expr

Equations

• Lean.instToExprInt16.mkNat n = Lean.mkApp3 (Lean.Expr.const `OfNat.ofNat [0]) (Lean.Expr.const `Int16 []) (Lean.mkRawNatLit n) ((Lean.Expr.const `Int16.instOfNat []).app (Lean.mkRawNatLit n))

instance Lean.instToExprInt32 : ToExpr Int32

Equations

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

def Lean.instToExprInt32.mkNat (n : Nat) : Expr

Equations

• Lean.instToExprInt32.mkNat n = Lean.mkApp3 (Lean.Expr.const `OfNat.ofNat [0]) (Lean.Expr.const `Int32 []) (Lean.mkRawNatLit n) ((Lean.Expr.const `Int32.instOfNat []).app (Lean.mkRawNatLit n))

instance Lean.instToExprInt64 : ToExpr Int64

Equations

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

def Lean.instToExprInt64.mkNat (n : Nat) : Expr

Equations

• Lean.instToExprInt64.mkNat n = Lean.mkApp3 (Lean.Expr.const `OfNat.ofNat [0]) (Lean.Expr.const `Int64 []) (Lean.mkRawNatLit n) ((Lean.Expr.const `Int64.instOfNat []).app (Lean.mkRawNatLit n))

instance Lean.instToExprISize : ToExpr ISize

Equations

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

def Lean.instToExprISize.mkNat (n : Nat) : Expr

Equations

• Lean.instToExprISize.mkNat n = Lean.mkApp3 (Lean.Expr.const `OfNat.ofNat [0]) (Lean.Expr.const `ISize []) (Lean.mkRawNatLit n) ((Lean.Expr.const `ISize.instOfNat []).app (Lean.mkRawNatLit n))

instance Lean.instToExprBool : 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 }

instance Lean.instToExprChar : ToExpr Char

Equations

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

instance Lean.instToExprString : ToExpr String

Equations

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

instance Lean.instToExprUnit : ToExpr Unit

Equations

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

instance Lean.instToExprFilePath : 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 }

instance Lean.instToExprName : ToExpr Name

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

instance Lean.instToExprLiteral : ToExpr Literal

Equations

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

instance Lean.instToExprFVarId : ToExpr 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 }

instance Lean.instToExprPreresolved : ToExpr Syntax.Preresolved

Equations

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

def Lean.Expr.toCtorIfLit : Expr → 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✝