idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-09-21 02:07:25 +03:00
Code Issues Projects Releases Wiki Activity

Add irrelevance annotations to Data.List functions taking NonEmpty

Browse Source
This commit is contained in:
Ohad Kammar 2020-07-30 06:01:42 +01:00
parent 5ad779f9de
commit 5cfbac4a51
1 changed files with 6 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
libs/base/Data/List.idr
View File

@ -327,21 +327,21 @@ Uninhabited (NonEmpty []) where
||| Get the head of a non-empty list.
||| @ ok proof the list is non-empty
public export
head : (l : List a) -> {auto ok : NonEmpty l} -> a
head : (l : List a) -> {auto 0 ok : NonEmpty l} -> a
head [] impossible
head (x :: _) = x
||| Get the tail of a non-empty list.
||| @ ok proof the list is non-empty
public export
tail : (l : List a) -> {auto ok : NonEmpty l} -> List a
tail : (l : List a) -> {auto 0 ok : NonEmpty l} -> List a
tail [] impossible
tail (_ :: xs) = xs
||| Retrieve the last element of a non-empty list.
||| @ ok proof that the list is non-empty
public export
last : (l : List a) -> {auto ok : NonEmpty l} -> a
last : (l : List a) -> {auto 0 ok : NonEmpty l} -> a
last [] impossible
last [x] = x
last (x::y::ys) = last (y::ys)
@ -349,7 +349,7 @@ last (x::y::ys) = last (y::ys)
||| Return all but the last element of a non-empty list.
||| @ ok proof the list is non-empty
public export
init : (l : List a) -> {auto ok : NonEmpty l} -> List a
init : (l : List a) -> {auto 0 ok : NonEmpty l} -> List a
init [] impossible
init [_] = []
init (x::y::ys) = x :: init (y::ys)
@ -440,14 +440,14 @@ mapMaybe f (x::xs) =
||| Foldl a non-empty list without seeding the accumulator.
||| @ ok proof that the list is non-empty
public export
foldl1 : (a -> a -> a) -> (l : List a) -> {auto ok : NonEmpty l} -> a
foldl1 : (a -> a -> a) -> (l : List a) -> {auto 0 ok : NonEmpty l} -> a
foldl1 f [] impossible
foldl1 f (x::xs) = foldl f x xs
||| Foldr a non-empty list without seeding the accumulator.
||| @ ok proof that the list is non-empty
public export
foldr1 : (a -> a -> a) -> (l : List a) -> {auto ok : NonEmpty l} -> a
foldr1 : (a -> a -> a) -> (l : List a) -> {auto 0 ok : NonEmpty l} -> a
foldr1 f [] impossible
foldr1 f [x] = x
foldr1 f (x::y::ys) = f x (foldr1 f (y::ys))