begin...end vs by{...}

Stream: new members

[Horatiu Cheval]

Is there a difference between a begin...end block and a by{...} block? I've been able to use them interchangeably so far.

Also, what exactly do they do? Am I correct to think of them as a kind of do block?

[Yakov Pechersky]

Yes, begin tactic1, tactic2 end or by tactic1; tactic2 or by {tactic1, tactic2} are all ways to enter tactic mode from term mode

[Yakov Pechersky]

And internally it is a docs#tactic is a monad because it is a interaction_monad tactic_state

[Bryan Gin-ge Chen]

In mathlib, our style guide suggests using by { ... } when we can squeeze things on one line, otherwise begin ... end is prefered.

by tactic1; tactic2 is slightly different from the other two, as it runs tactic2 on all goals created by tactic1. Thus in mathlib, we try to use it only when there really are multiple goals in play.

[Horatiu Cheval]

Thanks for the explanation! I have one more question here, does the comma we write between tactics have a specific meaning?
Is it a, let's say, tactic composition operator, such that {tactic1, tactic2} is a new tactic resulting from the two, or is it simply syntax to mark the end of tactic within tactic mode?

[Bryan Gin-ge Chen]

You can think of the comma as a composition operator if you want. Tactics are operations in the "tactic monad" which contains the proof state and lots of other goodies. You can read more about that here and in the other resources linked there.

[Kevin Buzzard]

I believe that {tac1, tac2} is a new tactic.

[Horatiu Cheval]

Ok, thanks!