Merge pull request #3 from mattpolzin/fix-build

Fix build

README.md

@@ -7,14 +7,12 @@ A Vect type that has the semantics of a reversed vector.
 
 You can depend on this package in one of 3 ways.
 
-### Sirdi
-If your project uses Sirdi, add the following dependency to your sirdi.json:
-```json
-{"name": "snocvect", "git": {"url": "https://github.com/mattpolzin/idris-snocvect"}}
-```
+### Pack
+Make sure you have Pack installed, `snocvect` in your package's dependencies
+list, and then build your project via Pack.
 
 ### Idris install
-You can clone this repository and run the following commands to install it into your local Idris 2 package directory:
+Clone this repository and run the following commands to install it into your local Idris 2 package directory:
 ```shell
 idris2 --build snocvect.ipkg
 idris2 --install snocvect.ipkg
@@ -23,4 +21,4 @@ idris2 --install snocvect.ipkg
 Then add it to your project's `ipkg` file under `depends` or use the `-p snocvect` flag when invoking `idris2`.
 
 ### Local dependency
-You can also build this package as described under the previous section but instead of installing it to your Idris 2 package directory you can copy the contents of the build/ttc folder into a `depends` directory within your project folder.
+Build this package as described under the previous section but instead of installing it to your Idris 2 package directory you can copy the contents of the build/ttc folder into a `depends` directory within your project folder.

snocvect.ipkg

@@ -1,7 +1,7 @@
 package snocvect
 sourcedir = "src"
 modules = Data.SnocVect, Data.SnocVect.Elem
-version = 0.1.0
+version = 0.2.0
 authors = "Mathew Polzin"
 license = "MIT"
 sourceloc = "https://github.com/mattpolzin/idris-snocvect"

src/Data/SnocVect.idr

@@ -17,8 +17,8 @@ data SnocVect : Nat -> Type -> Type where
 
 %name SnocVect sx, sy, sz
 
-infixl 7 <><
-infixr 6 <>>
+export infixl 7 <><
+export infixr 6 <>>
 
 ||| 'fish': Action of lists on snoc-lists
 public export

src/Data/SnocVect/Elem.idr

@@ -19,8 +19,8 @@ neitherHereNorThere : DecEq a => {0 x,y : a} ->
                       Not (x = y) ->
                       Not (Elem sy x) ->
                       Not (Elem (sy :< y) x)
-neitherHereNorThere Refl _ Here impossible
-neitherHereNorThere _ g (There z) = g z
+neitherHereNorThere _ notThere (There z) = notThere z
+neitherHereNorThere notHere _ Here = notHere Refl
 
 export
 isElem : DecEq a => (x : a) -> (sx : SnocVect k a) -> Dec (Elem sx x)