Stream: Coq users

Topic: scope of definitions in sections, modules


view this post on Zulip Philipp G. Haselwarter (Dec 03 2020 at 17:00):

When Ltac definitions and Scope declarations are made inside (1) a section or (2) a module, is that definition / scope accessible in some way after the section/module is closed?

view this post on Zulip Fabian Kunze (Dec 03 2020 at 19:04):

For a section, there is no hope for ltac-definitions to be visible outside (how would one generalize an tactic that is exact n for a section variable n after closing the section?). from a Module M, a tactic t defined in it is simply available as M.t (assuming you used Ltac t := ...).

view this post on Zulip Fabian Kunze (Dec 03 2020 at 19:07):

For scopes declaration, I'm not sure, but if a prefixedGlobal does not work, nothing does afaik.

view this post on Zulip Paolo Giarrusso (Dec 03 2020 at 23:05):

FWIW: almost everything works in a module, since everything is defined in a module.

view this post on Zulip Paolo Giarrusso (Dec 03 2020 at 23:08):

the main (huge) exception is that "nested" modules are always Required with their containing module, so side effects that act on Require can only be disabled on top-level modules (by not requiring them, not even transitively), but not on "nested" modules (since you always get them when you require the containing module).


Last updated: Jan 31 2023 at 14:03 UTC