Name generation

Stream: general

[Patrick Massot]

I have a meta-question about name generation. My tactic gets its hands on a type, and needs to choose a name for a term of that type. This is in a maths context so the type would typically be called X, and I would expect my tactic to choose x as a term type, appending some index if there is already x in my tactic state. I already know about get_unused_name so only the first step is really missing. Is there any example I could try to copy? There are bonus points if I can also decide that a term of type α should be called a but this is not mandatory.

[Rob Lewis]

Literally mapping X to x? char.to_lower or some version lifted to string? This will work for A-Z at least.

[Rob Lewis]

I'm pretty sure there's no function in mathlib to guess variable names more intelligently than that.

[Patrick Massot]

It would be better to have a slightly more robustness. The type could be X' for instance.

[Patrick Massot]

and then I'd like to get x'

[Rob Lewis]

You can map to_lower over the string.

[Rob Lewis]

But this feels a little un-mathlib to me. Usually, if a user is expected to deal with the local constants created by a tactic, they provide the names explicitly.

[Patrick Massot]

I agree, but this is not for mathlib.

[Patrick Massot]

Does anyone know how to rewrite in a tactic? All the function I'd like to use are marked as private in Lean core lib.

[Patrick Massot]

Nevermind, I found it.

[Patrick Massot]

There is a subtle game between rw_* and rewrite_*.