Merge pull request #4588 from clayrat/patch-13

Cons is not Nil
idris-lang · Nov 19, 2018 · a244099 · a244099
2 parents 347b63f + 7695883
commit a244099
Showing 1 changed file with 6 additions and 0 deletions.
diff --git a/libs/prelude/Prelude/List.idr b/libs/prelude/Prelude/List.idr
@@ -861,6 +861,12 @@ catMaybes (x::xs) =
 -- Properties
 --------------------------------------------------------------------------------
 
+Uninhabited ([] = _ :: _) where
+  uninhabited Refl impossible
+
+Uninhabited (_ :: _ = []) where
+  uninhabited Refl impossible
+
 ||| (::) is injective
 consInjective : {x : a} -> {xs : List a} -> {y : b} -> {ys : List b} ->
                 (x :: xs) = (y :: ys) -> (x = y, xs = ys)