Add postulates.

1 files changed, 8 insertions, 0 deletions

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
@@ -87,6 +87,13 @@ data NormalForm : Sorted.Family Relevance where
 %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
   name : WithBounds String
@@ -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''