Zulip Chat Archive

Stream: new members

Topic: Term Mode vs. Tactic Mode


view this post on Zulip William Sealy Gosset (Oct 12 2020 at 15:31):

When building out new areas of Mathlib, is there a preference for proofs in term mode or proofs in tactic mode?

view this post on Zulip Mario Carneiro (Oct 12 2020 at 15:33):

No, but most authors develop their own preference

view this post on Zulip Mario Carneiro (Oct 12 2020 at 15:34):

As a general rule of thumb, we use term mode for "one-liners" and tactic mode for longer proofs

view this post on Zulip William Sealy Gosset (Oct 12 2020 at 15:35):

@Mario Carneiro Thank you


Last updated: May 14 2021 at 03:27 UTC