From 0bcf7554e97b9b6fa3d7fcec97b095363450d182 Mon Sep 17 00:00:00 2001
From: Yusuke Matsushita <y.skm24t@gmail.com>
Date: Fri, 30 Apr 2021 16:28:28 +0000
Subject: [PATCH] Add functional notations for `dist`

---
 iris/algebra/ofe.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/iris/algebra/ofe.v b/iris/algebra/ofe.v
index 9219e4c43..01cbd49d8 100644
--- a/iris/algebra/ofe.v
+++ b/iris/algebra/ofe.v
@@ -18,6 +18,10 @@ 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).
+Notation "(≡{ n }≡)" := (dist n) (only parsing).
+Notation "(≡{ n }@{ A }≡)" := (dist (A:=A) n) (only parsing).
+Notation "( x ≡{ n }≡.)" := (dist n x) (only parsing).
+Notation "(.≡{ n }≡ y )" := (λ x, x ≡{n}≡ y) (only parsing).
 
 Global Hint Extern 0 (_ ≡{_}≡ _) => reflexivity : core.
 Global Hint Extern 0 (_ ≡{_}≡ _) => symmetry; assumption : core.
-- 
GitLab