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 denotesa
- toTypeExpr : Lean.Expr
Expression representing the type
α
Instances
- EquationsCommand.instToExprMagmaLawOfToLevel
- FBinopElab.instToExprSRec
- 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.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
- 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.Tactic.ITauto.instToExprAndKind
- Mathlib.Tactic.ITauto.instToExprIProp
- Mathlib.Tactic.ITauto.instToExprProof
- Mathlib.instToExprBinderInfo_mathlib
- Mathlib.instToExprExpr_mathlib
- Mathlib.instToExprFVarId_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
- Plausible.instToExprConfiguration
- Sat.instToExprLiteral
- instToExprBinderInfo_qq
- instToExprExpr_qq
- instToExprFVarId_qq
- instToExprLevelMVarId_qq
- instToExprLevel_qq
- instToExprLiteral_qq
- instToExprMData_qq
- instToExprMVarId_qq
- instToExprRArray
Equations
- Lean.instToExprNat = { toExpr := Lean.mkNatLit, toTypeExpr := Lean.mkConst `Nat }
Equations
- One or more equations did not get rendered due to their size.
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))
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.instToExprBool = { toExpr := fun (b : Bool) => if b = true then Lean.mkConst `Bool.true else Lean.mkConst `Bool.false, toTypeExpr := Lean.mkConst `Bool }
Equations
- Lean.instToExprChar = { toExpr := fun (c : Char) => Lean.mkApp (Lean.mkConst `Char.ofNat) (Lean.mkRawNatLit c.toNat), toTypeExpr := Lean.mkConst `Char }
Equations
- Lean.instToExprString = { toExpr := Lean.mkStrLit, toTypeExpr := Lean.mkConst `String }
Equations
- Lean.instToExprUnit = { toExpr := fun (x : Unit) => Lean.mkConst `Unit.unit, toTypeExpr := Lean.mkConst `Unit }
Equations
- Lean.instToExprFilePath = { toExpr := fun (p : System.FilePath) => Lean.mkApp (Lean.mkConst `System.FilePath.mk) (Lean.toExpr p.toString), toTypeExpr := Lean.mkConst `System.FilePath }
Equations
- Lean.instToExprName = { toExpr := Lean.Name.toExprAux, toTypeExpr := Lean.mkConst `Lean.Name }
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
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.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.instToExprFVarId = { toExpr := fun (fvarId : Lean.FVarId) => Lean.mkApp (Lean.mkConst `Lean.FVarId.mk) (Lean.toExpr fvarId.name), toTypeExpr := Lean.mkConst `Lean.FVarId }
Equations
- One or more equations did not get rendered due to their size.
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