Commit b16e3e3c authored by Robbert Krebbers's avatar Robbert Krebbers

Notation `≡{n}@{A}≡` to be explicit about the type in `≡{n}≡`.

parent 9e8c1030
......@@ -16,6 +16,9 @@ Class Dist A := dist : nat → relation A.
Instance: Params (@dist) 3.
Notation "x ≡{ n }≡ y" := (dist n x y)
(at level 70, n at next level, format "x ≡{ n }≡ y").
Notation "x ≡{ n }@{ A }≡ y" := (dist (A:=A) n x y)
(at level 70, n at next level, only parsing).
Hint Extern 0 (_ {_} _) => reflexivity : core.
Hint Extern 0 (_ {_} _) => symmetry; assumption : core.
Notation NonExpansive f := ( n, Proper (dist n ==> dist n) f).
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment