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/Term.idr | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

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

diff --git a/src/Obs/Term.idr b/src/Obs/Term.idr
index 5126d99..8829038 100644
--- a/src/Obs/Term.idr
+++ b/src/Obs/Term.idr
@@ -12,6 +12,8 @@ import Text.Bounded
 
 -- Definition ------------------------------------------------------------------
 
+infix 5 ::<
+
 data Term : Nat -> Type
 
 public export
@@ -73,6 +75,12 @@ data Term : Nat -> Type where
   Cast : (oldType, newType, equality, value : WithBounds (Term n)) -> Term n
   CastId : (value : WithBounds (Term n)) -> Term n
 
+public export
+record Parameter (n : Nat) where
+  constructor MkParameter
+  name : WithBounds String
+  ty : WithBounds (Term n)
+
 public export
 record Definition (n : Nat) where
   constructor MkDefinition
@@ -84,6 +92,7 @@ public export
 data Block : Nat -> Type where
   Nil  : Block 0
   (:<) : Block n -> Definition n -> Block (S n)
+  (::<) : Block n -> Parameter n -> Block (S n)
 
 -- Pretty Print ----------------------------------------------------------------
 
@@ -167,6 +176,11 @@ export
 Pretty (Term n) where
   prettyPrec = Term.prettyPrec
 
+export
+Pretty (Parameter n) where
+  pretty param = group $
+    pretty "parameter" <++> pretty param.name.val <++> colon <+> softline <+> pretty param.ty.val
+
 export
 Pretty (Definition n) where
   pretty def = group $
@@ -177,4 +191,6 @@ export
 Pretty (Block n) where
   pretty []           = neutral
   pretty ([] :< def)  = pretty def
+  pretty ([] ::< param)  = pretty param
   pretty (blk :< def) = pretty blk <+> hardline <+> hardline <+> pretty def
+  pretty (blk ::< param) = pretty blk <+> hardline <+> hardline <+> pretty param
-- 
cgit v1.2.3