let syntax () =
  let pr = Format.eprintf in
  pr "@[";
  pr "<term> ::= <var> @\n";  
  pr "         | <name> '(' <term> {',' <term>}* ')' >@\n";
  pr "         | <arith> | <tuple> | <array> | <sexpr> | <bv> | <boolean>@\n";
  pr "         | '(' <term> ')'@\n\n";
  pr "<var> ::= <ident> | <ident> '!' <int>@\n\n";
  pr "<arith> ::= <rational> | <term> {'+' | '-' | '*'} <term>@\n\n";
  pr "          | '-' <term> | <term> '^' <int>@\n";
  pr "<tuple> ::= '(' <term> {',' <term>}* ')'@\n";
  pr "          | 'proj[' <int> ',' <int> ']' '(' <term> ')'@\n\n";
  pr "<sexpr> ::= 'nil' | 'cons' '(' <term> ',' <term> ')'@\n";
  pr "          | {'car' | 'cdr'} '(' <term> ')'@\n\n";
  pr "<array> ::= <term> '[' <term> ':=' <term> ']'@\n";
  pr "          | <term> '[' <term> ']'@\n\n";
  pr "<boolean> ::= 'true' | 'false'@\n\n";
  pr "<bv> ::= '0b' {'0' | '1'}* | <term> '++' <term>@\n";
  pr "       | <term> '['<int>':'<int>']' '('<term>')'@\n";
  pr "       | <term> {'&&' | '||' | '##'} <term>@\n\n";
  pr "<atom> ::= 'tt' | 'ff' | <term> {'=' | '<>' | '<' | '>' | '<=' | '>='} <term>@\n";
  pr "<prop> ::= <atom> | '[' <prop> ']' | <prop> ['&' | '|' | '=>' | '<=>' | '#'] <prop>@\n";
  pr "           | '~'<prop>@\n | 'if' <prop> 'then' <prop> 'else' <prop> 'end'@\n";
  pr "<ident> ::=  ('A'|..|'Z'|'a'|..|'z') {'A'|..|'Z'|'a'|..|'z'|'\\''|'0'|..|'9'}*@\n";
  pr "<int> ::= {'0'|..|'9'}+@\n";
  pr "<rat> ::= <int> {'/' <int>}@\n\n";
  pr "Comments start with percent and end with a newline.@\n";
  pr "Identifiers do not include any keywords and command names.@\n";
  pr "Operator precedence in increasing order:@\n";
  pr "'-', '+', '*', '/', '^', '++', '||', '##', '&&'.@\n";
  pr "Conventions:@\n";
  pr "nonterminals: <..>@\n";
  pr "terminals:  '..'@\n";
  pr "choice: .. | ..@\n";
  pr "optional: { .. }@\n";
  pr "zero or more repetions: {..}*@\n";
  pr "one or more repetions: {..}+@\n";
  pr "@]@."