Fix Hangman example

idris-hackers · Mar 25, 2017 · 356a5aa · 356a5aa
1 parent bb29307
commit 356a5aa
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 5 deletions.
diff --git a/Hangman/hangman.idr → Hangman/Hangman.idr b/Hangman/hangman.idr → Hangman/Hangman.idr
diff --git a/Hangman/VectMissing.idr b/Hangman/VectMissing.idr
@@ -3,9 +3,7 @@ module VectMissing
 import Data.Fin
 import Data.Vect
 
-Uninhabited (Elem x []) where
-    uninhabited Here impossible
-
+public export
 shrink : (xs : Vect (S n) a) -> Elem x xs -> Vect n a
 shrink (x :: ys) Here = ys
 shrink (y :: []) (There p) = absurd p

diff --git a/Hangman/hangman.ipkg b/Hangman/hangman.ipkg
@@ -1,8 +1,8 @@
 package hangman
 
-modules = VectMissing, hangman 
+modules = VectMissing, Hangman 
 opts = "-p effects" 
 
 executable = hangman
-main = hangman
+main = Hangman