Zulip Chat Archive

Stream: general

Topic: refine and implicit constructors

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 :=
  refine λ hp, hq⟩, hq, hp⟩, λ hq, hp⟩, _⟩,
  exact hp, hq

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: Dec 20 2023 at 11:08 UTC