To make my files more readable, I’d like to use two notations:
- T <: U on one hand
- Ts <: vs :> Us on the other hand. For the curious, vs is about variance so this one reads as “forall i, Ti <: UI if vi is Invariant / Covariant and Ui <: Ti if vi is Invariant / Contravariant”
I’m a bit lost in the notation/priority two allow both notations to use the <: symbol.
Is this possible ? Or should I choose a different symbol for the latter ?
<: is already used for a cast using the bytecode virtual machine. You can overwrite it by redefining a notation
Notation "x <: y" := ... (at level 100).
Notation "x <: y >: z" := ... (at level 100, y at next level).
The level 100 is hard-wired in the camlp5 parser, so, this is why the
Notation mechanism does not already know it. The
at next level is to left-factorize the second rule with the first one (see the example of
x <= y <= z in
Great, thank you Hugo. It works very nicely !