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. Example:

toExpr true = .const ``Bool.true []

• toExpr : α → Lean.Expr

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

• toTypeExpr : Lean.Expr

  Expression representing the type α

Instances

• FBinopElab.instToExprSRec
• Fin.toExpr
• Lean.Elab.Tactic.Omega.instToExprConstraint
• Lean.Elab.Tactic.Omega.instToExprLinearCombo
• Lean.Meta.DiscrTree.instToExprKey
• Lean.Meta.Linear.Nat.instToExprLinearCnstr
• Lean.Meta.Linear.Nat.instToExprLinearExpr
• Lean.Meta.instToExprCoeFnInfo
• Lean.Meta.instToExprCoeFnType
• Lean.Position.instToExpr
• Lean.instToExprArray
• Lean.instToExprArrayOfToLevel
• Lean.instToExprBitVec
• Lean.instToExprBool
• Lean.instToExprChar
• Lean.instToExprDeclarationRange
• Lean.instToExprDeclarationRanges
• Lean.instToExprFVarId
• Lean.instToExprFilePath_mathlib
• Lean.instToExprFin
• Lean.instToExprInt
• Lean.instToExprList
• Lean.instToExprListOfToLevel
• Lean.instToExprLiteral
• Lean.instToExprName
• Lean.instToExprNat
• Lean.instToExprOption
• Lean.instToExprOptionOfToLevel
• Lean.instToExprPreresolved
• Lean.instToExprProd
• Lean.instToExprProdOfToLevel
• Lean.instToExprString
• Lean.instToExprUInt16
• Lean.instToExprUInt32
• Lean.instToExprUInt64
• Lean.instToExprUInt8
• Lean.instToExprUSize
• Lean.instToExprUnit
• Mathlib.instToExprBinderInfo_mathlib
• Mathlib.instToExprExpr_mathlib
• Mathlib.instToExprFVarId_mathlib
• Mathlib.instToExprInt_mathlib
• Mathlib.instToExprLevelMVarId_mathlib
• Mathlib.instToExprLevel_mathlib
• Mathlib.instToExprLiteral_mathlib
• Mathlib.instToExprMData_mathlib
• Mathlib.instToExprMVarId_mathlib
• Mathlib.instToExprPUnitOfToLevel
• Mathlib.instToExprPos_mathlib
• Mathlib.instToExprPreresolved_mathlib
• Mathlib.instToExprSourceInfo_mathlib
• Mathlib.instToExprSubstring_mathlib
• Mathlib.instToExprSyntax_mathlib
• Mathlib.instToExprULiftOfToLevel
• PiFin.toExpr
• instToExprBinderInfo_qq
• instToExprExpr_qq
• instToExprFVarId_qq
• instToExprFilePath_batteries
• instToExprInt_qq
• instToExprLevelMVarId_qq
• instToExprLevel_qq
• instToExprLiteral_qq
• instToExprMData_qq
• instToExprMVarId_qq

instance Lean.instToExprNat : Lean.ToExpr Nat

Equations

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

instance Lean.instToExprInt : Lean.ToExpr Int

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

instance Lean.instToExprUInt8 : Lean.ToExpr UInt8

Equations

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

instance Lean.instToExprUInt16 : Lean.ToExpr UInt16

Equations

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

instance Lean.instToExprUInt32 : Lean.ToExpr UInt32

Equations

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

instance Lean.instToExprUInt64 : Lean.ToExpr UInt64

Equations

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

instance Lean.instToExprUSize : Lean.ToExpr USize

Equations

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

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 }

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 }

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 : Unit) => Lean.mkConst `Unit.unit, toTypeExpr := Lean.mkConst `Unit }

instance Lean.instToExprName : Lean.ToExpr Lake.Name

Equations

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

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

Equations

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

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

Equations

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

instance Lean.instToExprArray {α : Type u_1} [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} [Lean.ToExpr α] [Lean.ToExpr β] : Lean.ToExpr (α × β)

Equations

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

instance Lean.instToExprLiteral : Lean.ToExpr Lean.Literal

Equations

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

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 }

instance Lean.instToExprPreresolved : Lean.ToExpr Lean.Syntax.Preresolved

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.