Skip to content

Commit

Permalink
docs: why replacePrefix2 is different
Browse files Browse the repository at this point in the history
  • Loading branch information
William Sørensen committed Aug 8, 2024
1 parent d904907 commit e5710e7
Showing 1 changed file with 9 additions and 2 deletions.
11 changes: 9 additions & 2 deletions Qpf/Macro/NameUtils.lean
Original file line number Diff line number Diff line change
@@ -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
Expand Down

0 comments on commit e5710e7

Please sign in to comment.