1 files changed, 16 insertions, 6 deletions
diff --git a/src/Obs/Parser.idr b/src/Obs/Parser.idr
index d0a9fb8..c1bd468 100644
--- a/src/Obs/Parser.idr
+++ b/src/Obs/Parser.idr
@@ -61,6 +61,7 @@ data ObsTokenKind
   | OTAOpen
   | OTAClose
   -- Other Symbols
+  | OTPostulate
   | OTComma
   | OTTilde
   | OTEqual
@@ -111,6 +112,7 @@ Eq ObsTokenKind where
   OTAOpen == OTAOpen = True
   OTAClose == OTAClose = True
 
+  OTPostulate == OTPostulate = True
   OTComma == OTComma = True
   OTTilde == OTTilde = True
   OTEqual == OTEqual = True
@@ -163,6 +165,7 @@ Show ObsTokenKind where
   show OTAOpen = "<"
   show OTAClose = ">"
 
+  show OTPostulate = "postulate"
   show OTComma = ","
   show OTTilde = "~"
   show OTEqual = "="
@@ -217,6 +220,7 @@ TokenKind ObsTokenKind where
   tokValue OTAOpen s = ()
   tokValue OTAClose s = ()
 
+  tokValue OTPostulate s = ()
   tokValue OTComma s = ()
   tokValue OTTilde s = ()
   tokValue OTEqual s = ()
@@ -261,6 +265,8 @@ keywords =
   , ("if", OTIf)
 
   , ("Container", OTContainer)
+
+  , ("postulate", OTPostulate)
   ]
 
 obsTokenMap : TokenMap ObsToken
@@ -453,20 +459,24 @@ def : Grammar state ObsToken True (WithBounds String, WithBounds Syntax)
 def = [| MkPair (ident <* whitespace <* match' OTEqual <* whitespace) exp |]
 
 partial
+param : Grammar state ObsToken True Parameter
+param = map (\(MkDecl name ty) => MkParameter {name, ty}) $
+  match OTPostulate *> commit *> whitespace *> decl exp
+
+partial
 fullDef : Grammar state ObsToken True Definition
 fullDef =
   seq
     [| MkPair (decl exp <* commit) (optional whitespace *> match' OTNewlines *> def <* commit) |]
     (\((MkDecl name ty), (name', tm)) =>
       if name.val == name'.val
-        then pure (MkDefinition {name = name, ty, tm})
+        then pure (MkDefinition {name, ty, tm})
         else fatalLoc name.bounds "name mismatch' for declaration and definition")
 
 partial
-file : Grammar state ObsToken False (List Definition)
-file =
-  optional (whitespace *> match' OTNewlines) *>
-  sepEndBy (optional whitespace *> match' OTNewlines) (fullDef <* commit)
+file : Grammar state ObsToken False (List (Either Parameter Definition))
+file = many (whitespace *> match' OTNewlines) *>
+  sepEndBy (optional whitespace *> match' OTNewlines) (choose param fullDef <* commit)
 
 whitespaceIrrelevant : WithBounds ObsToken -> WithBounds ObsToken
 whitespaceIrrelevant a = case (a.val.kind) of
@@ -495,7 +505,7 @@ castErr (Left errs) = do
 
 partial
 export
-parse : String -> Logging ann (List Definition)
+parse : String -> Logging ann (List (Either Parameter Definition))
 parse str = do
   let (toks, _, _, "") = lex obsTokenMap str
     | (toks, l, c, rem) => inScope "lex" $ do