ext1 vs ext : 1

Stream: general

[Patrick Massot]

Is there any difference between ext1 and ext : 1?

[Simon Hudon]

None

[Patrick Massot]

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

[Patrick Massot]

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

[Simon Hudon]

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

Not that I know of.

[Simon Hudon]

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]

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

[Patrick Massot]

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

[Simon Hudon]

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]

I think you're right about redundancy.

[Mario Carneiro]

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

[Simon Hudon]

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]

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]

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]

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

[Scott Morrison]

Absolutely! :-)