Extracted from parse2/Parser/PropParser.y on 20040901.
As in the Haskell 98 syntax reference:
Notation  Meaning 

[pattern]  optional 
{pattern}  zero or more repetitions 
(pattern)  grouping 
pat_{1}pat_{2}  choice 
assert
 terminal syntax 
assertion
and property
below, respectively.
assertion : assert [conid =] prop property : property conid {varcon} = formula prop : pqcon {predarg}  (All  Exist) var [:: ctype] . prop  / prop  prop propop prop  pexp === pexp  pexp ::: formula  ( prop ) propop : /\  \/  ==>  <==> pexp : { exp }  qvar  pqcon  literal formula : aformula  formula > formula  formula qconop formula  / formula  formula propop formula  Lfp conid . formula  Gfp conid . formula  pqcon {predarg} predarg : { exp }  qvar  literal  aformula aformula : pqcon  [ ]  ! aexp1  $ aformula  ( formulas )  { typedpats  prop } typedpats : typedpat { , typedpat } typedpat : pat [:: ctype] formulas : formula { , formula } pqconid : CONID  QCONID  tupcon pqcon : pqconid  ( gconsym )
assert
and
property
.
Apart from this, all valid Haskell 98 syntax remains valid in the extended
language.
All
,Exist
,Gfp
,Lfp
,
!
,.
,$
,/
,/\
,\/
,===
,==>
,<==>
There is a special comment syntax that can be used to mark assertions and other code that should be considered by the Programatica tools, but ignored by Haskell compilers:
{P:
...)
This syntax is seen as a comment by regular Haskell tools,
but treated as if the {P:
and
}
characters were spaces by the Programatica tools.
Associativity  Operator 

right  Gfp , Lfp ,
All , Exist

right  > , qconop

left  <==>

right  ==>

left  /\ , \/ , / ,
===

left  :::
