[ base ] add total last to List1

libs/base/Data/List.idr

@@ -318,7 +318,7 @@ public export
 last : (l : List a) -> {auto ok : NonEmpty l} -> a
 last [] impossible
 last [x] = x
-last (x::y::ys) = last (y::ys)
+last (x::y::ys) = List.last (y::ys)
 
 ||| Return all but the last element of a non-empty list.
 ||| @ ok proof the list is non-empty

libs/base/Data/List1.idr

@@ -8,6 +8,14 @@ record List1 a where
   head : a
   tail : List a
 
+export
+last : List1 a -> a
+last (x :: xs) = go x xs where
+
+  go : a -> List a -> a
+  go x [] = x
+  go _ (y :: ys) = go y ys
+
 public export
 toList : (1 xs : List1 a) -> List a
 toList (x :: xs) = x :: xs