Overloaded Operators for KeY lang

[wadoon]

This MR brings overloaded operators to KeY lang:

1. On function and predicate definitions you can additional add prefix, infix, and postfix notations.

   \functions {
     int add(int, int) \infix(+);
   }
   

   These information are stored inside the Function object.

2. These information also impacts the pretty printing.

3. Operators are now a sequence of symbols [-+*/^<>=|]. Their first character determines the precedence. Following are legal expressions:

     a ++ b + c  = ( a ++ b ) + c
     a <|> b <= c 
     a +- b != a + -b
   

This trick avoids an "operator precedence parser", which would also be nice.

[mattulbrich]

This MR brings overloaded operators to KeY lang:

Does this include overloading in the sense that several signatures can share the same symbol (+ for floats and for integers e.g.). That would really be important.

Update: Just browsed through the examples. It seems that: yes. Great!

[mattulbrich]

This seams to deviate from the PR description

[github-actions]

Thank you for your contribution.

The test artifacts are available on Artiweb.
The newest artifact is here.