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