Zulip Chat Archive
Stream: lean4
Topic: include & omit
Uranus Testing (Jun 28 2022 at 17:01):
There were include and omit keywords in Lean 3. Are there analogous in Lean 4?
Mario Carneiro (Jun 28 2022 at 21:24):
There are not. For the most part they are not needed anymore
Last updated: Dec 20 2023 at 11:08 UTC