Stream: Coq users

Topic: ✔ Notation, Hints and Sections


view this post on Zulip 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 ?

view this post on Zulip Vincent Siles (Dec 09 2021 at 15:27):

I'm scanning the doc but only find things about notation scopes (like :core)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Vincent Siles (Dec 09 2021 at 15:32):

Will do. Thanks !

view this post on Zulip Notification Bot (Dec 09 2021 at 16:19):

Vincent Siles has marked this topic as resolved.


Last updated: Jan 31 2023 at 12:01 UTC