git.iko.soy/Idris-dev
on master help sign in
Merge pull request #3902 from clayrat/master

mark covering functions using `sizeAccessible` as `public export total`

commit8ab4dc878a2bac542ee8a817f0054b378d9dad8a authorNiklas Larsson <metaniklas@gmail.com> dateSat 8 Jul 2017, 12:36 (9 years ago) parente819e6b06501c2
3 files changed+4−4
compare with master
unifiedsplit
libs/base/Data/List/Views.idr+2−2 libs/base/Data/Nat/Views.idr+1−1 libs/base/Data/Vect/Views.idr+1−1
libs/base/Data/List/Views.idr+2−2
@@ -63,7 +63,7 @@ data SplitRec : List a -> Type where
6363
6464||| Covering function for the `SplitRec` view
6565||| Constructs the view in O(n lg n)
66−export total
66+public export total
6767splitRec : (xs : List a) -> SplitRec xs
6868splitRec xs with (sizeAccessible xs)
6969 splitRec xs | acc with (split xs)
@@ -109,7 +109,7 @@ filteredROK p x xs = LTESucc (filterSmaller xs)
109109
110110||| Covering function for the `Filtered` view
111111||| Constructs the view in O(n lg n)
112−export
112+public export total
113113filtered : (p : a -> a -> Bool) -> (xs : List a) -> Filtered p xs
114114filtered p inp with (sizeAccessible inp)
115115 filtered p [] | _ = FNil
libs/base/Data/Nat/Views.idr+1−1
@@ -22,7 +22,7 @@ half (S k) with (half k)
2222 HalfEven {n=S n}
2323 half (S (n + n)) | HalfEven = HalfOdd
2424
25−export
25+public export total
2626halfRec : (n : Nat) -> HalfRec n
2727halfRec n with (sizeAccessible n)
2828 halfRec Z | acc = HalfRecZ
libs/base/Data/Vect/Views.idr+1−1
@@ -71,7 +71,7 @@ smallerPlusR {m} {k} = rewrite sym (plusSuccRightSucc m k) in
7171
7272||| Covering function for the `SplitRec` view
7373||| Constructs the view in O(n lg n)
74−export
74+public export total
7575splitRec : (xs : Vect n a) -> SplitRec xs
7676splitRec {n} input with (sizeAccessible n)
7777 splitRec input | acc with (split input)