Appending indices to Names

Stream: lean4

[Thomas Murrills]

Sometimes you'd like to take an existing Name and append a number to it. What's the best way of doing this? Using numerical names doesn't seem to work well, at least not in the context I'm interested in:

elab "newMVar" : term => mkFreshExprMVar none .synthetic (userName := .num `x 1)
example : Nat := by refine newMVar; case x.1 =>    -- error: "expected =>"

Is this a problem with case, or (I'm guessing) because numerical names aren't meant to be used this way?

If the latter, how would one turn a Name and a Nat into an indexed name, e.g. with a separating underscore?

[Tomas Skrivan]

Use Name.appendAfter function for this.

[Jannis Limperg]

And indeed the Name.num constructor is only used for internal names afaik.