CODEWITHSUNDEEP
coq
IsAdisplayName
IsAdisplayName

Reputation: 217

Problems adding new notation in Coq

I'm trying to define a new notation scope and add notation to this scope in Coq. I'm following the guidance of this page in the Coq manual (https://coq.inria.fr/refman/user-extensions/syntax-extensions.html).

I define my new scope with

Declare Scope myHoTT_scope.
Delimit Scope myHoTT_scope with my.

Later I want to add "*" as an infix operator to the scope. I do this with

Infix "*" := concat (at level 40 , left associativity) : myHoTT_scope.

where concat is an already defined function. Coq accepts all of this. It raises no errors or warning. However, if I run

Locate "*".

the only thing that is returned is the definition of "*" in type_scope and nat_scope. Additionally, if I try

Check (p * q)%my.

I just receive errors stating that p should be of type nat. I can't tell why Coq doesn't seem to pick up this new notation. I followed the instructions to the letter and Coq gives no errors.

** Edit **, I found the problem. I had the definition of the new notation tucked inside a Section so its definition was not accessible from outside the section. I guess it is not possible to define global notation from within a section?

Upvotes: 4

Views: 560

Answers (2)

Meven Lennon-Bertrand
Meven Lennon-Bertrand

Reputation: 1296

As you discovered yourself, indeed new notations inside a section cannot be forced to be global. At least, that’s what I understand from the reference manual here. And trying the export and global attributes to a notation command indeed fails.

Upvotes: 3

Théo Winterhalter
Théo Winterhalter

Reputation: 5108

You never said that * should be in your new scope. You have to precise it in the notation declaration.

Declare Scope myHoTT_scope.
Delimit Scope myHoTT_scope with my.

Infix "*" := concat (at level 40 , left associativity) : myHoTT_scope.

Afterwards the notation is indeed found by Locate and is usable with the %my delimiter. (Note that for me, Locate also finds the notation even if I don't put it in myHoTT_scope.)

Upvotes: 1

Related Questions