`set_fixity : string -> fixity -> unit`
STRUCTURE
SYNOPSIS
Allows the fixity of tokens to be updated.
LIBRARY
Parse
DESCRIPTION
The set_fixity function is used to change the fixity of single tokens. It implements this functionality rather crudely. When called on to set the fixity of t to f, it removes all rules mentioning t from the global (term) grammar, and then adds a new rule to the grammar. The new rule maps occurrences of t with the given fixity to terms of the same name.
FAILURE
This function fails if the new fixity causes a clash with existing rules, as happens if the precedence level of the specified fixity is already taken by rules using a fixity of a different type. Even if the application of set_fixity succeeds, it may cause the next subsequent application of the Term parsing function to complain about precedence conflicts in the operator precedence matrix. These problems may cause the parser to behave oddly on terms involving the token whose fixity was set. Excessive parentheses will usually cure even these problems.
EXAMPLE
After a new constant is defined, set_fixity can be used to give it an appropriate parse status:
```   - val thm = Psyntax.new_recursive_definition
prim_recTheory.num_Axiom "f"
(Term`(f 0 n = n) /\ (f (SUC n) m = SUC (SUC (f n m)))`);
> val thm =
|- (!n. f 0 n = n) /\ !n m. f (SUC n) m = SUC (SUC (f n m))
: thm
- set_fixity "f" (Infixl 500);
> val it = () : unit
- thm;
> val it =
|- (!n. 0 f n = n) /\ !n m. SUC n f m = SUC (SUC (n f m)) : thm
```
The same function can be used to alter the fixities of existing constants:
```   - val t = Term`2 + 3 + 4 - 6`;
> val t = `2 + 3 + 4 - 6` : term
- set_fixity "+" (Infixr 501);
> val it = () : unit
- t;
> val it = `(2 + 3) + 4 - 6` : term
- dest_comb (Term`3 - 1 + 2`);
> val it = (`\$- 3`, `1 + 2`) : term * term
```