Zulip Chat Archive
Stream: new members
Topic: Term Mode vs. Tactic Mode
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?
Mario Carneiro (Oct 12 2020 at 15:33):
No, but most authors develop their own preference
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
William Sealy Gosset (Oct 12 2020 at 15:35):
@Mario Carneiro Thank you
Last updated: Dec 20 2023 at 11:08 UTC