Fighting `parameters` in order/zorn

Stream: general

[Eric Wieser]

I want to add this statement just below src#zorn.chain.mono:

theorem chain.symm {α : Type u} {s : set α} {q : α → α → Prop} (h : chain q s) : chain (flip q) s :=
h.mono' (λ _ _, or.symm)

I know how to prove it, but right now I'm not able to state it properly; lean is not letting me pass the q argument to chain, even if I use @.

I know this is due to the parameters statement in this file; is there any way to override it for the scope of one lemma?

[Mario Carneiro]

I think by exact is a way to get around parameters, since parameters don't work in tactics

[Eric Wieser]

Yes, this works:

theorem chain.symm {α : Type u} {s : set α} {q : α → α → Prop} (h : by exact chain q s) :
  by exact chain (flip q) s :=
h.mono' (λ _ _, or.symm)

[Eric Wieser]

But perhaps I should just wait till the parameter-poisoned section is closed, and then add the definition after it

[Eric Wieser]

ping @Yaël Dillies, since this came up when reviewing your PR, #7362

[Yaël Dillies]

What exactly are parameters doing? Can't we either get rid of them or cancel them at some point (without closing the section, I mean)?

[Eric Rodriguez]

it's like variables but it lets it be fixed over the whole section

[Yaël Dillies]

Isn't variables section-wide too?

[Eric Rodriguez]

yes, but it's not fixed; say you have some type variables (α : Type*), and you have test_def := f α, then you can use test_def (α ⊕ α) somewhere else in the section, whilst that would error with parameters