use pack DB HEAD in CI

joelberkeley · Jan 5, 2024 · 27a4687 · 27a4687
1 parent c1bde4a
commit 27a4687
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 7 deletions.
diff --git a/.github/workflows/checks.yml b/.github/workflows/checks.yml
@@ -30,7 +30,9 @@ jobs:
         ./install_bazel.sh
         ./build.sh cpu
     - name: Build tests
-      run: pack --no-prompt build test.ipkg
+      run: |
+        pack switch HEAD
+        pack --no-prompt build test.ipkg
     - name: Run tests
       run: pack run test.ipkg
       env:

diff --git a/src/Util.idr b/src/Util.idr
@@ -146,12 +146,6 @@ namespace List
   inBoundsCons _ InFirst = InFirst
   inBoundsCons (_ :: ys) (InLater prf) = InLater (inBoundsCons ys prf)
 
-||| Concatenate lists of proofs.
-public export
-(++) : All p xs -> All p ys -> All p (xs ++ ys)
-[] ++ pys = pys
-(px :: pxs) ++ pys = px :: (pxs ++ pys)
-
 ||| Apply a function to the environment of a reader.
 export
 (>$<) : (env' -> env) -> Reader env a -> Reader env' a