Commit 2022-04-26 13:58 c01494c6

View on Github →

feat: more expr traversal functions (#263)

split Mathlib/Lean/Expr into multiple files.
implement a version of replaceRecM that correctly instantiates free vars.
some additonal Expr functions These are prereqs of #234 and #229

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Lean/Expr.lean

deleted def Lean.BinderInfo.brackets

deleted def Lean.Expr.constName

deleted def Lean.Expr.getAppFnArgs

deleted def Lean.Expr.natLit!

deleted def Lean.Name.mapPrefix

Created Mathlib/Lean/Expr/Basic.lean

added def Lean.BinderInfo.brackets

added def Lean.ConstantInfo.isDef

added def Lean.ConstantInfo.isThm

added def Lean.ConstantInfo.toDeclaration!

added def Lean.ConstantInfo.updateName

added def Lean.ConstantInfo.updateType

added def Lean.ConstantInfo.updateValue

added def Lean.Expr.bvarIdx?

added def Lean.Expr.constName

added def Lean.Expr.getAppFnArgs

added def Lean.Expr.getArg?

added def Lean.Expr.getRevArg?

added def Lean.Expr.listNamesWithPrefix

added def Lean.Expr.modifyAppArg

added def Lean.Expr.modifyAppArgM

added def Lean.Expr.modifyArg

added def Lean.Expr.modifyArgM

added def Lean.Expr.modifyRevArg

added def Lean.Expr.natLit!

added def Lean.Name.mapPrefix

Modified Mathlib/Lean/Expr/ReplaceRec.lean

added def Lean.Expr.replaceRecM

added def Lean.Expr.replaceRecMeta

Modified Mathlib/Lean/Expr/Traverse.lean

added def Lean.Expr.traverseApp

added def Lean.Meta.traverseChildren

added def Lean.Meta.traverseForall

added def Lean.Meta.traverseLambda

added def Lean.Meta.traverseLet