Zulip Chat Archive

Stream: general

Topic: Horned a appearing in docs


view this post on Zulip Yakov Pechersky (Nov 12 2020 at 22:01):

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

view this post on Zulip Yakov Pechersky (Nov 12 2020 at 22:01):

Which is generated by simps

view this post on Zulip Mario Carneiro (Nov 12 2020 at 22:07):

I don't see the problem with this

view this post on Zulip Kevin Buzzard (Nov 12 2020 at 22:07):

it looks very odd

view this post on Zulip Mario Carneiro (Nov 12 2020 at 22:08):

I think this is a necessary result of having autogenerated lemmas

view this post on Zulip Mario Carneiro (Nov 12 2020 at 22:08):

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

view this post on Zulip Adam Topaz (Nov 12 2020 at 22:08):

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.

view this post on Zulip Mario Carneiro (Nov 12 2020 at 22:09):

an autogenerated lemma needs autogenerated names

view this post on Zulip Mario Carneiro (Nov 12 2020 at 22:09):

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

view this post on Zulip Adam Topaz (Nov 12 2020 at 22:09):

But why?

view this post on Zulip Adam Topaz (Nov 12 2020 at 22:10):

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

view this post on Zulip Mario Carneiro (Nov 12 2020 at 22:10):

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

view this post on Zulip Mario Carneiro (Nov 12 2020 at 22:10):

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

view this post on Zulip Adam Topaz (Nov 12 2020 at 22:11):

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

view this post on Zulip Mario Carneiro (Nov 12 2020 at 22:12):

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

view this post on Zulip Mario Carneiro (Nov 12 2020 at 22:12):

you can also use case to name your variables btw

view this post on Zulip Adam Topaz (Nov 12 2020 at 22:12):

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

view this post on Zulip Mario Carneiro (Nov 12 2020 at 22:14):

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

view this post on Zulip Mario Carneiro (Nov 12 2020 at 22:15):

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

view this post on Zulip Adam Topaz (Nov 12 2020 at 22:15):

It was x_ih_ᾰ_1 in my case


Last updated: May 16 2021 at 05:21 UTC