diff options
Diffstat (limited to 'src/Obs/Term.idr')
| -rw-r--r-- | src/Obs/Term.idr | 11 |
1 files changed, 9 insertions, 2 deletions
diff --git a/src/Obs/Term.idr b/src/Obs/Term.idr index d5213d2..2cc2f93 100644 --- a/src/Obs/Term.idr +++ b/src/Obs/Term.idr @@ -12,9 +12,12 @@ import Text.PrettyPrint.Prettyprinter public export data Term : Nat -> Type where - Var : Bounds -> Fin n -> Term n + Var : Bounds -> Fin n -> Term n -- Sorts - Sort : Bounds -> Sort -> Term n + Sort : Bounds -> Sort -> Term n + -- True + Top : Bounds -> Term n + Point : Bounds -> Term n public export record Definition (n : Nat) where @@ -35,6 +38,8 @@ export fullBounds : Term n -> Bounds fullBounds (Var x i) = x fullBounds (Sort x s) = x +fullBounds (Top x) = x +fullBounds (Point x) = x -- Pretty Print ---------------------------------------------------------------- @@ -42,6 +47,8 @@ export Pretty (Term n) where prettyPrec d (Var x i) = pretty "$\{show i}" prettyPrec d (Sort x s) = prettyPrec d s + prettyPrec d (Top x) = pretty "()" + prettyPrec d (Point x) = pretty "_" export Pretty (Definition n) where |