Commit 7e7adcb9 authored by Robbert Krebbers's avatar Robbert Krebbers

Notation for n-ary non-expansive functions.

parent dc6db28b
Pipeline #1482 passed with stage
......@@ -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.
......
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