Commit 2021-12-09 16:23 cc793ef4

View on Github →

feat(*): some auxiliary definitions for toAdditive (#112)

Define some extra functions about List, String, Name, Binder and Expr (ported from Lean 3)
Move some definitions about Expr from Tactic/Core to Lean/Expr.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Array/Defs.lean

added def Array.range

added def Array.reduceOption

Created Mathlib/Data/List/Defs.lean

added def List.mapIdx

added def List.mapIdxM

added def List.reduceOption

Modified Mathlib/Data/String/Defs.lean

added def String.mapTokens

Created Mathlib/Lean/Expr.lean

added def Lean.BinderInfo.brackets

added def Lean.Expr.constName

added def Lean.Expr.getAppFnArgs

added def Lean.Expr.natLit!

added def Lean.Name.mapPrefix

Modified Mathlib/Tactic/Core.lean

deleted def Lean.Expr.getAppFnArgs

deleted def Lean.Expr.natLit!

added def Lean.setProtected