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

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

diff --git a/src/Obs/NormalForm.idr b/src/Obs/NormalForm.idr
index b4b9f94..d325f1a 100644
--- a/src/Obs/NormalForm.idr
+++ b/src/Obs/NormalForm.idr
@@ -86,6 +86,13 @@ data NormalForm : Sorted.Family Relevance where
 %name Neutral t, u, v
 %name NormalForm t, u, v
 
+public export
+record Parameter (ctx : List Relevance) where
+  constructor MkParameter
+  name : WithBounds String
+  sort : Universe
+  ty : TypeNormalForm ctx
+
 public export
 record Definition (ctx : List Relevance) where
   constructor MkDefinition
@@ -98,6 +105,7 @@ public export
 data Context : List Relevance -> Type where
   Nil  : Context []
   (:<) : Context ctx -> (def : Definition ctx) -> Context (relevance def.sort :: ctx)
+  (::<) : Context ctx -> (param : Parameter ctx) -> Context (relevance param.sort :: ctx)
 
 %name Context ctx, ctx', ctx''
 
-- 
cgit v1.2.3