From a8a4ef9933a1a07b6fbf2d257df2a5fb40b1e87d Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Wed, 21 Dec 2022 20:32:56 +0000
Subject: Add sum types.

---
 src/Obs/Sort.idr | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'src/Obs/Sort.idr')

diff --git a/src/Obs/Sort.idr b/src/Obs/Sort.idr
index 70d5ed2..bbd6975 100644
--- a/src/Obs/Sort.idr
+++ b/src/Obs/Sort.idr
@@ -42,6 +42,11 @@ suc : Sort -> Sort
 suc Prop    = Set 0
 suc (Set i) = Set (S i)
 
+public export
+ensureSet : Sort -> Sort
+ensureSet Prop    = Set 0
+ensureSet (Set i) = Set i
+
 public export
 lub : Sort -> Sort -> Sort
 lub Prop    s'      = s'
-- 
cgit v1.2.3