From 8eddb5e439005a1abf73703d58bb1c7749ca5807 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Sat, 17 Dec 2022 10:56:43 +0000
Subject: Add pretty printing.

---
 obs.ipkg         | 2 ++
 src/Obs/Sort.idr | 8 ++++++++
 2 files changed, 10 insertions(+)

diff --git a/obs.ipkg b/obs.ipkg
index f556fef..229fbe6 100644
--- a/obs.ipkg
+++ b/obs.ipkg
@@ -2,5 +2,7 @@ package obs
 authors = "Greg Brown"
 sourcedir = "src"
 
+depends = contrib
+
 modules
   = Obs.Sort
diff --git a/src/Obs/Sort.idr b/src/Obs/Sort.idr
index 16eaa96..281a053 100644
--- a/src/Obs/Sort.idr
+++ b/src/Obs/Sort.idr
@@ -1,5 +1,7 @@
 module Obs.Sort
 
+import Text.PrettyPrint.Prettyprinter
+
 -- Definition ------------------------------------------------------------------
 
 public export
@@ -23,6 +25,12 @@ Show Sort where
   show (Set 0)     = "Set"
   show (Set (S i)) = "Set \{show (S i)}"
 
+export
+Pretty Sort where
+  prettyPrec d Prop        = pretty "Prop"
+  prettyPrec d (Set 0)     = pretty "Set"
+  prettyPrec d (Set (S i)) = parenthesise (d >= App) $ pretty "Set \{show (S i)}"
+
 -- Operations ------------------------------------------------------------------
 
 infix 5 ~>
-- 
cgit v1.2.3