Zulip Chat Archive

Stream: new members

Topic: What does include clause do

view this post on Zulip Sebasti√°n Galkin (Aug 15 2020 at 20:24):

I see code in mathlib doing the following:

variables {mM : monoid M} {mN : monoid N}

include mM mN

What does include achieve exactly?

More generally? Where could I read about this type of thing? I couldn't find it on the reference manual.

view this post on Zulip Bryan Gin-ge Chen (Aug 15 2020 at 20:26):

See https://leanprover.github.io/theorem_proving_in_lean/interacting_with_lean.html#more-on-sections

Last updated: May 08 2021 at 04:14 UTC