From eb49ef28b93431d9694a17b1ad44d9ea966bcb05 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Sat, 7 Jan 2023 22:01:05 +0000
Subject: Add postulates.

---
 src/Obs/Syntax.idr | 11 +++++++++++
 1 file changed, 11 insertions(+)

(limited to 'src/Obs/Syntax.idr')

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
-- 
cgit v1.2.3