Stream: general

Topic: ext1 vs ext : 1

Patrick Massot (Sep 28 2018 at 19:45):

Is there any difference between ext1 and ext : 1?

None

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

Patrick Massot (Sep 28 2018 at 19:48):

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

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.

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?

Patrick Massot (Sep 28 2018 at 19:52):

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

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

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?

Simon Hudon (Sep 28 2018 at 19:54):

I think you're right about redundancy.

Mario Carneiro (Sep 28 2018 at 19:57):

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

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

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

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. :-)

Simon Hudon (Sep 28 2018 at 23:44):

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

Scott Morrison (Sep 28 2018 at 23:45):

Absolutely! :-)

Last updated: May 10 2021 at 18:22 UTC