diff --git a/Qpf/Macro/NameUtils.lean b/Qpf/Macro/NameUtils.lean index c9bddfc..3f41546 100644 --- a/Qpf/Macro/NameUtils.lean +++ b/Qpf/Macro/NameUtils.lean @@ -1,9 +1,16 @@ open Lean Meta namespace Lean.Name --- This function has diffreent behaviour from Name.replacePrefix +/-- + This function has different behaviour from Name.replacePrefix that can be viewed in the following example: + + #eval replacePrefix `a `b `a.b -- `a + #eval replacePrefix2 `a `b `a.b -- `b.b + + This comes from the internal declaration of replacePrefix dropping the last named value before continuing +-/ def replacePrefix2 (old_pref new_pref : Name) : Name → Name - | Name.anonymous => Name.anonymous + | Name.anonymous => .anonymous | Name.str p s => let p' := if p == old_pref then new_pref else replacePrefix2 old_pref new_pref p Name.mkStr p' s