Help with notations that "look alike"

Using Coq
1

Hi !
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 ?

2

Hi Vincent,

Note that <: 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 Notations.v).

1 Like
3

Great, thank you Hugo. It works very nicely !