Ssreflect Users Discussion List

[Georges Gonthier <>]

  Well, according to the declared Coq grammar, {n | P n} + {forall n, ~ P n} 
should be a parsing error, and the parentheses around the forall are 
mandatory, because the "special" { x } notation is declared with x at level 
99, while forall n, ~ P n is parsed at level 200. Indeed Coq always prints 
back the forall with parentheses.
  My guess is that when there are no other rules that factor with { x .... 
Camlp5 recovers from the error silently because it has no alternative parse, 
whereas it issues a diagnostic when it thinks the user might have meant one 
of the Ssreflect notations. Changing the parse level of the Ssreflect 
notation will disable them altogether because the { x ... would then always 
have precedence, so the proper fix would be to respect the precedence 
declared in Init/Notations.v and not rely on undocumented error recovery in 
camlp5.
    Best,
Georges

-----Original Message-----
From:  
[] On Behalf Of Assia Mahboubi
Sent: 26 September 2014 17:25
To: 
Subject: [ssreflect] Sumbool notation

Hi,

I recently realized that :

Require Import ssreflect.

breaks the curly braces notations associated with sumbool and sumor, when 
they are used with keywords like for instance forall and exists.

Indeed the following script:

Require Import ssreflect.
Definition test (P : nat -> Prop) :=
  {n | P n} + {forall n, ~ P n}.

raises:

Syntax error: 'type' 'of' expected after '{' (in [constr:operconstr]).

The solution is to add extra parentheses like in:

Require Import ssreflect.
Definition test (P : nat -> Prop) :=
  {n | P n} + {(forall n, ~ P n)}.

This is caused by ssreflect.v declaring (l.240) :

Notation "{ 'type' 'of' c 'for' s }" := (dependentReturnType c s)
  (at level 0, format "{ 'type'  'of'  c  'for'  s }") : type_scope.

which seems to clash with the notations declared in the prelude 
(Init/Notations.v), where it is said that {_} + {_} is composed of { _ }, 
which has a "special status" and _ + _ which has level 50.

This blind attempt to fix the problem works (of course without requiring 
ssreflect):

Notation "{ 'type' 'of' c 'for' s }" := (c = s)
  (at level 1, format "{ 'type'  'of'  c  'for'  s }") : type_scope.

Require Import ssreflect.
Definition test (P : nat -> Prop) :=
  {n | P n} + {forall n, ~ P n}.

But why it works remains a bit of mystery to me. I would be very glad to have 
an explanation of these behaviours.

Thanks in advance,

assia