Skip to content

Notations for relations with explicit type arguments

Robbert Krebbers requested to merge robbert/rel_disambig into master

We discussed this already here: https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/134

The consensus was that @{A} would be a good fit, and would not cause conflicts. I implemented it here for hopefully all relations in std++: =, , , , , ##, , ≡ₚ, and adopted the code at many places to make use of these notations.

Merge request reports