From 7e7adcb991ab24b7636fdf5c91a19eaa796f2e6c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 17 Jun 2016 10:21:01 +0200
Subject: [PATCH] Notation for n-ary non-expansive functions.

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

diff --git a/algebra/cofe.v b/algebra/cofe.v
index 193e2103c..826db7356 100644
--- a/algebra/cofe.v
+++ b/algebra/cofe.v
@@ -216,6 +216,10 @@ Arguments CofeMor {_ _} _ {_}.
 Add Printing Constructor cofeMor.
 Existing Instance cofe_mor_ne.
 
+Notation "'λne' x .. y , t" :=
+  (@CofeMor _ _ (λ x, .. (@CofeMor _ _ (λ y, t) _) ..) _)
+  (at level 200, x binder, y binder, right associativity).
+
 Section cofe_mor.
   Context {A B : cofeT}.
   Global Instance cofe_mor_proper (f : cofeMor A B) : Proper ((≡) ==> (≡)) f.
-- 
GitLab