From 6e1f9a26990af458fb8f2001039e4495c7bc71c8 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 11 Mar 2021 13:00:38 +0100
Subject: [PATCH] Add notation for `singleton` with `disj_union`.
---
theories/base.v | 4 ++++
1 file changed, 4 insertions(+)
diff --git a/theories/base.v b/theories/base.v
index 81f9078b..2b00af03 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -866,6 +866,10 @@ Notation "{[ x ; y ; .. ; z ]}" :=
(union .. (union (singleton x) (singleton y)) .. (singleton z))
(at level 1) : stdpp_scope.
+Notation "+{[ x ; y ; .. ; z ]}" :=
+ (disj_union .. (disj_union (singleton x) (singleton y)) .. (singleton z))
+ (at level 1) : stdpp_scope.
+
Class SubsetEq A := subseteq: relation A.
Global Hint Mode SubsetEq ! : typeclass_instances.
Instance: Params (@subseteq) 2 := {}.
--
GitLab