## Tokens and operator priority

There are five composite operators: /\ (AND) and \/ (OR) and -> (IMPL) and <= (LE) and >= (GE). And three keywords: in (IN) and not (NOT) and sqrt (SQRT).

Numbers are either written with a binary representation, or with a decimal representation. In both representations, the {integer} parts are radix-10 natural numbers.

binary        {integer}([bB][-+]?{integer})?
decimal       (({integer}(\.{integer}?)?)|(\.{integer}))([eE][-+]?{integer})?
number        ({binary}|{decimal}|{hexadecimal})

These three expressions represent the same number: 57.5e-1, 23b-2, 0x5.Cp0. They do not have the same semantic for Gappa though and a different property will be proved in the decimal case. Indeed, some decimal numbers cannot be expressed as a dyadic number and Gappa will have to harden the proof and add a layer to take this into account. In particular, the user should refrain from being inventive with the constant 1. For example, writing this constant as 00100.000e-2 may prevent some rewriting rules to be applied.

Identifiers (IDENT) are matched by {alpha}({alpha}|{digit}|_)*.

The associativity and priority of the operators in logical formulas is as follows. It is meant to match the usual conventions.

%right IMPL
%left OR
%left AND
%left NOT

For the mathematical expressions, the priority are as follows. Note that NEG is the priority of the unary minus; this is the operator with the highest precedence.

%left '+' '-'
%left '*' '/'
%left NEG