diff options
Diffstat (limited to 'src/Obs/Syntax.idr')
| -rw-r--r-- | src/Obs/Syntax.idr | 22 |
1 files changed, 15 insertions, 7 deletions
diff --git a/src/Obs/Syntax.idr b/src/Obs/Syntax.idr index 056c86a..07c625b 100644 --- a/src/Obs/Syntax.idr +++ b/src/Obs/Syntax.idr @@ -11,12 +11,15 @@ import Text.PrettyPrint.Prettyprinter public export data Syntax : Type where - Var : Bounds -> String -> Syntax + Var : Bounds -> String -> Syntax -- Sorts - Sort : Bounds -> Sort -> Syntax + Sort : Bounds -> Sort -> Syntax -- True - Top : Bounds -> Syntax - Point : Bounds -> Syntax + Top : Bounds -> Syntax + Point : Bounds -> Syntax + -- False + Bottom : Bounds -> Syntax + Absurd : Bounds -> Syntax -> Syntax -> Syntax public export record Definition where @@ -31,9 +34,14 @@ record Definition where export Pretty Syntax where prettyPrec d (Var x str) = pretty str - prettyPrec d (Sort x s) = prettyPrec d s - prettyPrec d (Top x) = pretty "()" - prettyPrec d (Point x) = pretty "_" + prettyPrec d (Sort x s) = prettyPrec d s + prettyPrec d (Top x) = pretty "()" + prettyPrec d (Point x) = pretty "_" + prettyPrec d (Bottom x) = pretty "Void" + prettyPrec d (Absurd x a t) = + parenthesise (d > Open) $ + group $ + fillSep [pretty "absurd", prettyPrec App a, prettyPrec App t] export Pretty Definition where |