From b6fb551360b283c38b3ede9ef3e6d2922bd62b58 Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Sun, 18 Dec 2022 12:00:01 +0000 Subject: Add the True type. --- src/Obs/Syntax.idr | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) (limited to 'src/Obs/Syntax.idr') diff --git a/src/Obs/Syntax.idr b/src/Obs/Syntax.idr index 71d070f..da2f9e4 100644 --- a/src/Obs/Syntax.idr +++ b/src/Obs/Syntax.idr @@ -11,9 +11,12 @@ 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 public export record Definition where @@ -28,6 +31,8 @@ record Definition where fullBounds : Syntax -> Bounds fullBounds (Var x str) = x fullBounds (Sort x s) = x +fullBounds (Top x) = x +fullBounds (Point x) = x -- Pretty Print ---------------------------------------------------------------- @@ -35,6 +40,8 @@ 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 "_" export Pretty Definition where -- cgit v1.2.3