# Help with notations that "look alike"

**URL:** <https://discourse.rocq-prover.org/t/help-with-notations-that-look-alike/1580>\
**Category:** Using Rocq\
**Created:** [March 3, 2022, 9:53am UTC](https://discourse.rocq-prover.org/t/help-with-notations-that-look-alike/1580 "2022-03-03T09:53:19Z")\
**Posts on this page:** 3\
**Page:** 1

<div class="post-metadata">

**Author:** ![vsiles](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/vsiles/32/274_2.png) [@vsiles](https://discourse.rocq-prover.org/u/vsiles)\
**Post date:** [March 3, 2022, 9:53am UTC](https://discourse.rocq-prover.org/t/help-with-notations-that-look-alike/1580/1 "2022-03-03T09:53:19Z")

</div>

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 ?

---

<div class="post-metadata">

**Author:** ![herbelin](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/herbelin/32/111_2.png) [@herbelin](https://discourse.rocq-prover.org/u/herbelin)\
**Post date:** [March 4, 2022, 9:09am UTC](https://discourse.rocq-prover.org/t/help-with-notations-that-look-alike/1580/2 "2022-03-04T09:09:14Z")

</div>

Hi Vincent,

Note that `<:` is already used for a cast using the bytecode virtual machine. You can overwrite it by redefining a notation

```auto
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`).

---

<div class="post-metadata">

**Author:** ![vsiles](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/vsiles/32/274_2.png) [@vsiles](https://discourse.rocq-prover.org/u/vsiles)\
**Post date:** [March 4, 2022, 12:17pm UTC](https://discourse.rocq-prover.org/t/help-with-notations-that-look-alike/1580/3 "2022-03-04T12:17:48Z")

</div>

> [@herbelin](#):
>
> ```auto
> Notation "x <: y" := ... (at level 100).
> Notation "x <: y >: z" := ... (at level 100, y at next level).
> 
> ```

Great, thank you Hugo. It works very nicely !