separating goals

Stream: new members

[Patrick Thomas]

Are there alternatives to using {} to separate goals?

[Eric Wieser]

Why do you ask?

[Eric Wieser]

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

[Patrick Thomas]

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

[Eric Wieser]

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

[Patrick Thomas]

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]

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]

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

[Mario Carneiro]

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]

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]

At this point it is mostly for my own benefit.