summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGreg Brown <greg.brown01@ed.ac.uk>2022-12-17 10:56:43 +0000
committerGreg Brown <greg.brown01@ed.ac.uk>2022-12-17 10:56:43 +0000
commit8eddb5e439005a1abf73703d58bb1c7749ca5807 (patch)
tree84ee5a8c0c04a249b35f9e0bcc6fe4e3b6641820
parent29c2714d5b5eddf053579d66d20c88daa7cd4859 (diff)
Add pretty printing.
-rw-r--r--obs.ipkg2
-rw-r--r--src/Obs/Sort.idr8
2 files changed, 10 insertions, 0 deletions
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 ~>