Zulip Chat Archive
Stream: mathlib4
Topic: include/omit
Kevin Buzzard (Nov 05 2022 at 03:34):
Does mathlib4 or lean4 have include/omit? Mathbin is generating it for me, but I can't find it.
Mario Carneiro (Nov 05 2022 at 03:39):
No, it's in the Mathport/Syntax.lean file
Mario Carneiro (Nov 05 2022 at 03:39):
Lean 4 has made the majority of uses of include/omit unnecessary, so we are waiting to see whether we still need it
Last updated: Dec 20 2023 at 11:08 UTC