Zulip Chat Archive

Stream: new members

Topic: separating goals


Patrick Thomas (Oct 16 2021 at 18:25):

Are there alternatives to using {} to separate goals?

Eric Wieser (Oct 16 2021 at 19:41):

Why do you ask?

Eric Wieser (Oct 16 2021 at 19:42):

You could maybe use docs#tactic.interactive.solve1 directly, but it would be less clear

Patrick Thomas (Oct 16 2021 at 19:45):

I was looking for something more compact, like ++ in Coq.

Eric Wieser (Oct 16 2021 at 22:35):

Can you give an example of how that's more compact?

Patrick Thomas (Oct 17 2021 at 20:30):

I currently use braces as:

by_cases ...,
{
  ...
  ...
},
{
  ...
  ...
}

I would probably use something like ++ as:

by_cases ...,
++ ...
   ...
++ ...
   ...

It's not really a big deal though.

Alex J. Best (Oct 17 2021 at 20:32):

I don't think this exists in lean 3, it does in lean 4 though (which is altogether more whitespace sensitive).
Most people format their braces like this though, which is a bit more like the second option layout wise:

by_cases ...,
{ ...
  ... },
{ ...
  ...}

Patrick Thomas (Oct 17 2021 at 20:38):

To be honest, that doesn't appeal to me as much. Thank you though.

Mario Carneiro (Oct 17 2021 at 21:02):

The lean 4 style looks like this:

theorem foo : ... := by
  by_cases ...
  · tac
    tac
  · tac
    tac

It's not likely to change in lean 3 at this point.

Eric Wieser (Oct 17 2021 at 21:24):

The main appeal of using the {} style mentioned above is that if you get used to it then you will find over half a million lines of mathlib code easier to read. If you intend to collaborate, it's way more important to confirm to the community style than pick the one that's most appealing.

Of course, if you're writing code only for your own benefit, you're free to format it as you please

Patrick Thomas (Oct 17 2021 at 21:38):

At this point it is mostly for my own benefit.


Last updated: Dec 20 2023 at 11:08 UTC