Ssreflect Users Discussion List

[Assia Mahboubi <>]

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