Closed andylokandy closed 2 years ago
Added some trivial functions (basically from Data.Vect and Idris1) to Data.List:
last : (l : List a) -> {auto ok : NonEmpty l} -> a
last' : List a -> Maybe a
init : (l : List a) -> {auto ok : NonEmpty l} -> List a
init' : List a -> Maybe (List a)
unfold: (f : a -> Maybe a) -> (x : a) -> List a
foldl1 : (a -> a -> a) -> (l : List a) -> {auto ok : NonEmpty l} -> a
foldr1 : (a -> a -> a) -> (l : List a) -> {auto ok : NonEmpty l} -> a
foldl1' : (a -> a -> a) -> List a -> Maybe a
foldr1' : (a -> a -> a) -> List a -> Maybe a
Added some trivial functions (basically from Data.Vect and Idris1) to Data.List:
last : (l : List a) -> {auto ok : NonEmpty l} -> alast' : List a -> Maybe ainit : (l : List a) -> {auto ok : NonEmpty l} -> List ainit' : List a -> Maybe (List a)unfold: (f : a -> Maybe a) -> (x : a) -> List afoldl1 : (a -> a -> a) -> (l : List a) -> {auto ok : NonEmpty l} -> afoldr1 : (a -> a -> a) -> (l : List a) -> {auto ok : NonEmpty l} -> afoldl1' : (a -> a -> a) -> List a -> Maybe afoldr1' : (a -> a -> a) -> List a -> Maybe a