def Auto.ToExprExtra.instToExprNat_auto : Lean.ToExpr Nat

Equations

• Auto.ToExprExtra.instToExprNat_auto = { toExpr := fun (n : Nat) => Lean.Expr.lit (Lean.Literal.natVal n), toTypeExpr := Lean.Expr.const `Nat [] }

def Auto.ToExprExtra.instToExprInt_auto : Lean.ToExpr Int

Equations

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

def Auto.ToExprExtra.instExprToExprId (ty : Lean.Expr) : Lean.ToExpr Lean.Expr

Used when the elements of a container are already expressions For example, consider the ordinary l₁ := toExpr (a : List Nat) l₂ := (a : List Nat).map toExpr We require that toExpr (self:=instExprToExprId (.const ``Nat [])) l₂ ≝ l₁ It is obvious that this shouldn't be marked as an instance

Equations

• Auto.ToExprExtra.instExprToExprId ty = { toExpr := id, toTypeExpr := ty }