Zulip Chat Archive

Stream: new members

Topic: SetLike docs using Lean 3 or 4 syntax?

Martin C. Martin (Oct 26 2023 at 18:47):

Mathlib4's SetLike/Basic.lean contains this example usage in a comment:

instance : SetLike (MySubobject X) X :=
  MySubobject.carrier, λ p q h, by cases p; cases q; congr'

Is that proper Lean 4 syntax? OneShot translated my equivalent to:

  MySubobject.carrier, fun p q h => by cases p <;> cases q <;> congr

Which is correct?

Ruben Van de Velde (Oct 26 2023 at 19:16):

Most likely you'll get a warning that the <;> is unnecessary (though it will work)

Ruben Van de Velde (Oct 26 2023 at 19:17):

<;> and ; are only different if the tactic before it created multiple goals, which I'm guessing cases doesn't do in this case

Kyle Miller (Oct 26 2023 at 19:34):

Lean 3's ; is Lean 4's <;>, but I think the Lean 3 should have been written as by { cases p, cases q, congr' } (too frequently people used ; to avoid needing to reach for the braces)

Kyle Miller (Oct 26 2023 at 19:35):

I think the Lean 4 could be by cases p; cases q; congr! since p and q are structures, and since congr! is the analogue of congr' (it might make a difference if the structures have things like Decidable fields)

Anne Baanen (Oct 27 2023 at 14:06):

I tested Kyle's suggestion on Subgroup and that worked. So: #7986.

Last updated: Dec 20 2023 at 11:08 UTC