Vincent Siles (Dec 09 2021 at 15:18): Vincent Siles (Dec 09 2021 at 15:18):I have a file with a section with a few Notation and Hint Constructors : core. I'm Require Importing this file in another one, but my notations and hints doesn't seem available. Do I have to do something in the first file to make notations and hitns available outside of the file/section ?
Vincent Siles (Dec 09 2021 at 15:27):I'm scanning the doc but only find things about notation scopes (like :core)
Enrico Tassi (Dec 09 2021 at 15:28):From https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#basic-notations
This command supports the local attribute, which limits its effect to the current module. If the command is inside a section, its effect is limited to the section.
Théo Winterhalter (Dec 09 2021 at 15:30):It's because notations and tactics do not have a straightforward generalisation. The only solution is to define them again after closing the section.
Vincent Siles (Dec 09 2021 at 15:32):Will do. Thanks !
Notification Bot (Dec 09 2021 at 16:19):Vincent Siles has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC