Bind notation with type annotation

[alxest]

In usual Coq development, it is often useful to annotate a variable with its type (for better readability, error localization, better inference, etc), like:

Check (exists n, n = 0).
Check (exists (n: Z), n = 0).

Can we do similar thing with bind notation? like:

Check (x <- Ret tt ;; Ret x).
Check ((x: unit) <- Ret tt; Ret x).

My current workaround is like this:

Check (x <- Ret tt ;; let _ := x: unit in Ret x).

[YaZko]

We could certainly add another notation. The trivial PR #175 would allow you to write:

Import ITreeNotations.
Definition foo := unit.
Check (x <- Ret tt ;; Ret x).
Check (`x: foo <- Ret tt;; Ret x).

Note the necessary back-tick, as far as I can tell without it that would break all other type annotations.

[Lysxia]

@alxest is that a good fix for you?

[alxest]

@YaZko @Lysxia Yes, it works well for me. Thanks a lot!
I will close the issue.