diff options
author | Greg Brown <greg.brown01@ed.ac.uk> | 2022-12-17 10:56:43 +0000 |
---|---|---|
committer | Greg Brown <greg.brown01@ed.ac.uk> | 2022-12-17 10:56:43 +0000 |
commit | 8eddb5e439005a1abf73703d58bb1c7749ca5807 (patch) | |
tree | 84ee5a8c0c04a249b35f9e0bcc6fe4e3b6641820 | |
parent | 29c2714d5b5eddf053579d66d20c88daa7cd4859 (diff) |
Add pretty printing.
-rw-r--r-- | obs.ipkg | 2 | ||||
-rw-r--r-- | src/Obs/Sort.idr | 8 |
2 files changed, 10 insertions, 0 deletions
@@ -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 ~> |