Zulip Chat Archive

Stream: general

Topic: ext1 vs ext : 1


view this post on Zulip Patrick Massot (Sep 28 2018 at 19:45):

Is there any difference between ext1 and ext : 1?

view this post on Zulip Simon Hudon (Sep 28 2018 at 19:46):

None

view this post on Zulip Patrick Massot (Sep 28 2018 at 19:47):

Do we want to advertise ext1 then? This is different from asking whether it should exist as an internal part of ext

view this post on Zulip Patrick Massot (Sep 28 2018 at 19:48):

Do we have other tactics taking a natural number parameter introduced by :?

view this post on Zulip Simon Hudon (Sep 28 2018 at 19:51):

Do we have other tactics taking a natural number parameter introduced by :?

Not that I know of.

view this post on Zulip Simon Hudon (Sep 28 2018 at 19:51):

Do we want to advertise ext1 then? This is different from asking whether it should exist as an internal part of ext

What do you mean by advertise?

view this post on Zulip Patrick Massot (Sep 28 2018 at 19:52):

It's an interactive tactic, and it's mentioned in the docs

view this post on Zulip Patrick Massot (Sep 28 2018 at 19:52):

I'm a bit worried that we have more and more tactics to learn (thanks!) and redundancy may become a small problem

view this post on Zulip Simon Hudon (Sep 28 2018 at 19:53):

So if we were to stop advertising it, we'd take it out of tactic.interactive and remove it from the docs? Or maybe just mention it as part of the doc of ext?

view this post on Zulip Simon Hudon (Sep 28 2018 at 19:54):

I think you're right about redundancy.

view this post on Zulip Mario Carneiro (Sep 28 2018 at 19:57):

Is there really no difference? I would have guessed ext1 forces an application of extensionality

view this post on Zulip Simon Hudon (Sep 28 2018 at 19:58):

Initially that was the difference but @Scott Morrison found it more useful if ext would fail if it can't apply at least one extentionality lemma

view this post on Zulip Simon Hudon (Sep 28 2018 at 20:00):

With regards to learning tactics, we way want to categorize the ones that we have to make them a bit easier to learn

view this post on Zulip Scott Morrison (Sep 28 2018 at 23:41):

Categorizing them is a good idea. Our approach to documenting new tactics introduced in mathlib so far has been essentially an append-only list of paragraphs describing tactics. :-)

view this post on Zulip Simon Hudon (Sep 28 2018 at 23:44):

It's still better than before @Patrick Massot started his crusade: most are now documented :D

view this post on Zulip Scott Morrison (Sep 28 2018 at 23:45):

Absolutely! :-)


Last updated: May 10 2021 at 18:22 UTC