git.iko.soy/Idris-dev
on master help sign in
Added export and totality directives (#4360)
b93fe6bbadbadboy
libs/contrib/Data/List/Group.idr+3
compare with master
unifiedsplit
@@ -1,5 +1,8 @@
1module Data.List.Group
1module Data.List.Group
2
2
3+%default total
4+%access export
5+
3||| The groupBy function returns a list of lists such that the concatenation
6||| The groupBy function returns a list of lists such that the concatenation
4||| of the list is equal to the argument, and each sublist contains only
7||| of the list is equal to the argument, and each sublist contains only
5||| elements that are equal according to the user-supplied predicate.
8||| elements that are equal according to the user-supplied predicate.
libs/contrib/Data/List/Permutations.idr+2
@@ -1,5 +1,7 @@
1module Permutations
1module Permutations
2
2
3+%access export
4+
3-- | All permutations of a list.
5-- | All permutations of a list.
4permutations : List a -> List (List a)
6permutations : List a -> List (List a)
5permutations [] = [[]]
7permutations [] = [[]]