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))
Instances For
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