Closed alxest closed 4 years ago
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.
@alxest is that a good fix for you?
@YaZko @Lysxia Yes, it works well for me. Thanks a lot! I will close the issue.
In usual Coq development, it is often useful to annotate a variable with its type (for better readability, error localization, better inference, etc), like:
Can we do similar thing with bind notation? like:
My current workaround is like this: