Horned a appearing in docs

Stream: general

[Yakov Pechersky]

Like in docs#subtype.map_coe due to the way the lemma is stated.

[Yakov Pechersky]

Which is generated by simps

[Mario Carneiro]

I don't see the problem with this

[Kevin Buzzard]

it looks very odd

[Mario Carneiro]

I think this is a necessary result of having autogenerated lemmas

[Mario Carneiro]

we used to write these manually, and when you do so you can calibrate the presentation

[Adam Topaz]

I must be out of the loop. What's going on with this funny "a"? It came up as an automatically generated name for an inductive hypothesis in some proof I was working on today, and I had no idea how to typeset it.

[Mario Carneiro]

an autogenerated lemma needs autogenerated names

[Mario Carneiro]

the funny "a" is just the new default base name for autogenerated names

[Adam Topaz]

But why?

[Adam Topaz]

Is it to discourage people from referring to the auto-generated name?

[Mario Carneiro]

it's there to discourage accidental use, as well as fixing the longstanding a bug

[Mario Carneiro]

which was basically where people would choose themselves a name that overlaps the one the name generator wanted to pick

[Adam Topaz]

Well, I guess it did it's job in my case :rofl: Except instead of using induction foo with h1 h2 ... I just copied/pasted from the goal window

[Mario Carneiro]

I think mathlib has a style linter that will complain at you if you write ᾰ in a mathlib file

[Mario Carneiro]

you can also use case to name your variables btw

[Adam Topaz]

(To clarify, this was just experimenting during a discussion with a student, not in anything intended for mathlib)

[Mario Carneiro]

maybe we should have a tactic that renames all the variables starting with ᾰ to a provided list

[Mario Carneiro]

that would help in the few cases where you can't easily supply the name because it is deep in some tactic that doesn't thread the names through, like finish or tidy

[Adam Topaz]

It was x_ih_ᾰ_1 in my case