@@ -52,13 +52,12 @@ data NonEmpty : (xs : List a) -> Type where
5252 ||| The proof that a cons cell is non-empty
5353 IsNonEmpty : NonEmpty (x :: xs)
5454
55−private
56−nonEmptyNil : NonEmpty [] -> Void
57−nonEmptyNil IsNonEmpty impossible
55+instance Uninhabited (NonEmpty []) where
56+ uninhabited IsNonEmpty impossible
5857
5958||| Decide whether a list is non-empty
6059nonEmpty : (xs : List a) -> Dec (NonEmpty xs)
61−nonEmpty [] = No nonEmptyNil
60+nonEmpty [] = No absurd
6261nonEmpty (x :: xs) = Yes IsNonEmpty
6362
6463||| Satisfiable if `k` is a valid index into `xs`