From d75ef7a07ac545433b92f721244da8207cc244be Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 20 Dec 2014 11:05:13 -0800
Subject: [PATCH] feat(hott/init/types): add 'sum' notation

---
 hott/init/types/sum.hlean | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)
 create mode 100644 hott/init/types/sum.hlean

diff --git a/hott/init/types/sum.hlean b/hott/init/types/sum.hlean
new file mode 100644
index 0000000000..664a2b5e65
--- /dev/null
+++ b/hott/init/types/sum.hlean
@@ -0,0 +1,17 @@
+/-
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura, Jeremy Avigad
+-/
+prelude
+import init.datatypes init.reserved_notation
+
+namespace sum
+  notation A ⊎ B := sum A B
+  notation A + B := sum A B
+  namespace low_precedence_plus
+    reserve infixr `+`:25  -- conflicts with notation for addition
+    infixr `+` := sum
+  end low_precedence_plus
+end sum