Simplifications

MathiasVP · Mar 27, 2018 · 2b20ea0 · 2b20ea0
1 parent b19c5c9
commit 2b20ea0
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/README.md b/README.md
@@ -5,7 +5,7 @@ The grammar is given by `RegExp: Type -> Type`.
 The semantics of regular expressions is specified by
 
 ```idris
-RegExpSpec: (RegExp a) -> (xs: List a) -> Type
+RegExpSpec: RegExp a -> List a -> Type
 ```
 
 Finally the file contains a verified matching procedure for deciding regular language membership

diff --git a/regex.idr b/regex.idr
@@ -12,7 +12,7 @@ data RegExp: Type -> Type where
   Empty: RegExp a
   Nothing: RegExp a
 
-data RegExpSpec: (RegExp a) -> (xs: List a) -> Type where
+data RegExpSpec: RegExp a -> List a -> Type where
   AtomSpec: (x : a) -> RegExpSpec (Atom x) [x]
   DisjSpec1: (r1 : RegExp a) ->
              (r2: RegExp a) -> (xs : List a) ->
@@ -39,7 +39,7 @@ data RegExpSpec: (RegExp a) -> (xs: List a) -> Type where
              RegExpSpec (Star r) zs
   EmptySpec: RegExpSpec Empty []
 
-isEmpty : (r : RegExp a) -> RegExp a
+isEmpty : RegExp a -> RegExp a
 isEmpty (Atom x) = Nothing
 isEmpty (Disj x y) = Disj (isEmpty x) (isEmpty y)
 isEmpty (Seq x y) = Seq (isEmpty x) (isEmpty y)