Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-02-05 14:13 a0d8ae1e

View on Github →

feat(tactic/replaceable): supplement def_replacer with attribute replaceable

Estimated changes

Modified src/data/string.lean

deleted def string.map_tokens

Created src/data/string/defs.lean

added def string.map_tokens

added def string.over_list

Modified src/meta/expr.lean

added def name.append_suffix

Modified src/tactic/replacer.lean