From 29c2714d5b5eddf053579d66d20c88daa7cd4859 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Sat, 17 Dec 2022 10:26:37 +0000
Subject: Define sorts.

---
 obs.ipkg         |  3 ++-
 src/Obs.idr      |  0
 src/Obs/Sort.idr | 44 ++++++++++++++++++++++++++++++++++++++++++++
 3 files changed, 46 insertions(+), 1 deletion(-)
 delete mode 100644 src/Obs.idr
 create mode 100644 src/Obs/Sort.idr

diff --git a/obs.ipkg b/obs.ipkg
index 4a5cafc..f556fef 100644
--- a/obs.ipkg
+++ b/obs.ipkg
@@ -2,4 +2,5 @@ package obs
 authors = "Greg Brown"
 sourcedir = "src"
 
-modules = Obs
+modules
+  = Obs.Sort
diff --git a/src/Obs.idr b/src/Obs.idr
deleted file mode 100644
index e69de29..0000000
diff --git a/src/Obs/Sort.idr b/src/Obs/Sort.idr
new file mode 100644
index 0000000..16eaa96
--- /dev/null
+++ b/src/Obs/Sort.idr
@@ -0,0 +1,44 @@
+module Obs.Sort
+
+-- Definition ------------------------------------------------------------------
+
+public export
+data Sort : Type where
+  Prop : Sort
+  Set  : Nat -> Sort
+
+%name Sort s, s', s'', s'''
+
+-- Interfaces ------------------------------------------------------------------
+
+export
+Eq Sort where
+  Prop    == Prop    = True
+  (Set i) == (Set j) = True
+  _       == _       = False
+
+export
+Show Sort where
+  show Prop        = "Prop"
+  show (Set 0)     = "Set"
+  show (Set (S i)) = "Set \{show (S i)}"
+
+-- Operations ------------------------------------------------------------------
+
+infix 5 ~>
+
+public export
+suc : Sort -> Sort
+suc Prop    = Set 0
+suc (Set i) = Set (S i)
+
+public export
+lub : Sort -> Sort -> Sort
+lub Prop    s'      = s'
+lub (Set i) Prop    = Set i
+lub (Set i) (Set j) = Set (max i j)
+
+public export
+(~>) : Sort -> Sort -> Sort
+s ~> Prop    = Prop
+s ~> (Set k) = lub s (Set k)
-- 
cgit v1.2.3