new behaviour of ext?

Stream: general

[Scott Morrison]

Hi @Simon Hudon, did the behaviour of ext just change? I'm finding the hypotheses of my ext lemmas being added as goals in a different order than previously.

[Mario Carneiro]

ext did change. could you be more specific about the difference?

[Scott Morrison]

Sorry, I think actually nothing changed, but I would like to propose a change!

[Scott Morrison]

When you apply, there is an option to control the order of the introduced goals.

[Scott Morrison]

The default is "dependent first", with the idea that fulfilling these may magically clear the later ones.

[Scott Morrison]

I find that instead it's more likely to give me confusing goals with metavariables, and I would prefer to explain the non-dependent goals first!

[Simon Hudon]

The order of assumptions should not have changed. What might have changed is the exact extensionality rule that gets applied. For instance, we're trying to avoid funext if set.ext is more relevent. I'm hoping this should make your proofs more stable even as the set of extensionality lemmas changes with time.