Zulip Chat Archive

Stream: new members

Topic: begin...end vs by{...}


view this post on Zulip Horatiu Cheval (Feb 11 2021 at 15:27):

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?

view this post on Zulip Yakov Pechersky (Feb 11 2021 at 16:02):

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

view this post on Zulip Yakov Pechersky (Feb 11 2021 at 16:05):

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

view this post on Zulip Bryan Gin-ge Chen (Feb 11 2021 at 16:07):

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.

view this post on Zulip Horatiu Cheval (Feb 12 2021 at 08:00):

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?

view this post on Zulip Bryan Gin-ge Chen (Feb 12 2021 at 08:06):

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.

view this post on Zulip Kevin Buzzard (Feb 12 2021 at 08:06):

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

view this post on Zulip Horatiu Cheval (Feb 12 2021 at 08:21):

Ok, thanks!


Last updated: May 13 2021 at 23:16 UTC