CODEWITHSUNDEEP
coq
Kristian
Kristian

Reputation: 1737

Add notation to a scope globally in Coq

I am having trouble defining some notation globally. I am trying to define some notation in a scope within a module, and I would like to have it available in other modules, but I cannot make this happen.

For example, if i write

Declare Scope scope0.
Declare Scope scope1.
Declare Scope scope2.

Module A.

  Notation ". A" := (list A) (at level 100) : scope0.
  #[global]
  Notation ". A" := (list A) (at level 100) : scope1.
  #[local]
  Notation ". A" := (list A) (at level 100) : scope2.

  Print Scope scope0.
  Print Scope scope1.
  Print Scope scope2.

End A.

Module B.

  Print Scope scope0.
  Print Scope scope1.
  Print Scope scope2.

End B.

Then the three first Print Scope shows that the notation is present in the scope, but in the last three ones it is gone again, and I cannot use it.

When I read the documentation of Notation I got the impression that it should not be local to a module.

Upvotes: 2

Views: 278

Answers (2)

Théo Winterhalter
Théo Winterhalter

Reputation: 5108

As a principle, things defined in a module are not available outside of it unless you Require/Import the module to make it available in scope. The distinction between local and global—unless I'm mistaken—is more related to what is indeed available outside of the module when it is imported.

In the case of notations you have to import the module for them to be available. So you would need

Import A.

in your module B.

Upvotes: 2

Kristian
Kristian

Reputation: 1737

I found the answer, namely that I should import the module after closing it. That is, with

Declare Scope scope0.
Module A.
  Notation ". A" := (list A) (at level 100) : scope0.
End A.

Import A.

Module B.
  Print Scope scope0.
End B

The notation is also available in module B, and the Print Scope statement lists it.

I found it by reading about the Import command where is says:

Some features defined in modules are activated only when a module is imported. This is for instance the case of notations (see Notations).

and gave examples where modules were imported right after they were closed.

There might be other ways of doing it, but this was the one I found.

Upvotes: 2

Related Questions