summaryrefslogtreecommitdiff
path: root/src/Obs/Syntax.idr
diff options
context:
space:
mode:
Diffstat (limited to 'src/Obs/Syntax.idr')
-rw-r--r--src/Obs/Syntax.idr11
1 files changed, 11 insertions, 0 deletions
diff --git a/src/Obs/Syntax.idr b/src/Obs/Syntax.idr
index 868e761..ea7772e 100644
--- a/src/Obs/Syntax.idr
+++ b/src/Obs/Syntax.idr
@@ -72,6 +72,12 @@ record Definition where
ty : WithBounds Syntax
tm : WithBounds Syntax
+public export
+record Parameter where
+ constructor MkParameter
+ name : WithBounds String
+ ty : WithBounds Syntax
+
-- Pretty Print ----------------------------------------------------------------
prettyPrecBounds : Prec -> WithBounds Syntax -> Doc ann
@@ -159,3 +165,8 @@ Pretty Definition where
pretty def = group $
pretty def.name.val <++> colon <+> softline <+> pretty def.ty.val <+> hardline <+>
pretty def.name.val <++> equals <+> softline <+> pretty def.tm.val
+
+export
+Pretty Parameter where
+ pretty param = group $
+ pretty "parameter" <++> pretty param.name.val <++> colon <+> softline <+> pretty param.ty.val