safeTail.idr

data NonEmptyList : List a -> Type where
  NonEmpty : NonEmptyList (x :: xs)

safeTail : (xs : List a) -> {auto prf : NonEmptyList xs} -> List a
safeTail (_ :: xs) = xs

test : List Int
test = [1, 2, 3]

-- type error, empty list
-- badTail : List Int
-- badTail = safeTail []

goodTail : List Int
goodTail = safeTail [1, 2, 3]