From 17f4c74e4cf7cfae631140246c243a1c16f93afb Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 21 Feb 2019 09:44:42 +0100
Subject: [PATCH] Operational type class for disjoint union.

---
 theories/base.v | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/theories/base.v b/theories/base.v
index e0034cc2..522ef574 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -782,6 +782,14 @@ Definition union_list `{Empty A} `{Union A} : list A → A := fold_right (∪) 
 Arguments union_list _ _ _ !_ / : assert.
 Notation "⋃ l" := (union_list l) (at level 20, format "⋃  l") : stdpp_scope.
 
+Class DisjUnion A := disj_union: A → A → A.
+Hint Mode DisjUnion ! : typeclass_instances.
+Instance: Params (@disj_union) 2 := {}.
+Infix "⊎" := disj_union (at level 50, left associativity) : stdpp_scope.
+Notation "(⊎)" := disj_union (only parsing) : stdpp_scope.
+Notation "( x ⊎)" := (disj_union x) (only parsing) : stdpp_scope.
+Notation "(⊎ x )" := (λ y, disj_union y x) (only parsing) : stdpp_scope.
+
 Class Intersection A := intersection: A → A → A.
 Hint Mode Intersection ! : typeclass_instances.
 Instance: Params (@intersection) 2 := {}.
-- 
GitLab