## Stream: general

### Topic: Name generation

#### Patrick Massot (Dec 04 2019 at 17:13):

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 (Dec 04 2019 at 17:18):

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

#### Rob Lewis (Dec 04 2019 at 17:19):

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

#### Patrick Massot (Dec 04 2019 at 17:19):

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

#### Patrick Massot (Dec 04 2019 at 17:20):

and then I'd like to get x'

#### Rob Lewis (Dec 04 2019 at 17:20):

You can map to_lower over the string.

#### Rob Lewis (Dec 04 2019 at 17:21):

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 (Dec 04 2019 at 17:22):

I agree, but this is not for mathlib.

#### Patrick Massot (Dec 04 2019 at 17:35):

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 (Dec 04 2019 at 17:40):

Nevermind, I found it.

#### Patrick Massot (Dec 04 2019 at 17:40):

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

Last updated: May 17 2021 at 22:15 UTC