Eric Rodriguez (Oct 30 2021 at 11:51):
it's always made me sad that stuff like this:
example (p q : Prop) : p ∧ q ↔ q ∧ p := begin refine ⟨λ ⟨hp, hq⟩, ⟨hq, hp⟩, λ ⟨hq, hp⟩, _⟩, exact ⟨hp, hq⟩ end
doesn't work. is this a technical limitation? fixable in lean4?
Floris van Doorn (Oct 30 2021 at 22:42):
Oh, I didn't even know this was an issue. This looks like something that is fixable (but maybe not worth it in Lean 3), without knowing the details.
It's very possible that this issue has rarely been encountered before, because you're combining
refine (tactic mode) with the term mode
λ ⟨hq, hp⟩, which is then usually written with
cases, since you were in tactic mode anyway.
Yaël Dillies (Oct 30 2021 at 23:01):
Oh really? I thought this was well-known because I literally pester it three times a day.
Yaël Dillies (Oct 30 2021 at 23:02):
This arbitrary rule has been impressed to the very core of my soul and I always look out for it.
Last updated: Aug 03 2023 at 10:10 UTC