The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

2016-08-23 16:54 GMT+02:00 Guillaume Melquiond 
<guillaume.melquiond AT inria.fr>:
> On 23/08/2016 16:15, Beta Ziliani wrote:
>> Hi list,
>>
>> We've been fighting this issue for way too long, and now it's time to
>> ask the crowd. We like to override the notation for lists /only/ when
>> the list is the argument of certain definition. However, the notation is
>> being pervasive to every list. Aren’t scopes intended for that? What is
>> wrong with our understanding of scopes?

> Open scopes only control whether you need to explicitly tell Coq which
> interpretation scope to use (using %scope). They have no impact on
> whether a notation is enabled or disabled (be it for parsing or printing).

However intuitively one would think that when printing the choice of
notation is the one that needs no % at parsing (top of the scope
stack). And this is not the case.

[...]
Close Scope patterns_scope.
Close Scope pattern_scope.

(* Definition foo := ((with 0| 1| 2 end)). (* Fails, needs %patterns *) *)
Definition alist := [0;1;2]. (* succeeds withtout % *)
Print alist. (* (with 0| 1| 2 end)%patterns *)

This is rather confusing isn't it?

Strangely if one moves the "Import ListNotation" AFTER the "Close
Scope", it behaves more or less as expected... Except that:

Definition amatch := mmatch 0 with 0 => 1 | 1 => 2 end.
Print amatch.  ===> amatch = mmatch 0 ([(0 => 1)%pattern; (1 => 2)%pattern])

%patterns


P.


> Best regards,
>
> Guillaume