git.iko.soy/Idris-dev
on master help sign in
mark covering functions using `sizeAccessible` as `public export total`
06501c2Alex Gryzlov
libs/base/Data/List/Views.idr+2−2
compare with master
unifiedsplit
@@ -63,7 +63,7 @@ data SplitRec : List a -> Type where
63
63
64||| Covering function for the `SplitRec` view
64||| Covering function for the `SplitRec` view
65||| Constructs the view in O(n lg n)
65||| Constructs the view in O(n lg n)
66−export total
66+public export total
67splitRec : (xs : List a) -> SplitRec xs
67splitRec : (xs : List a) -> SplitRec xs
68splitRec xs with (sizeAccessible xs)
68splitRec xs with (sizeAccessible xs)
69 splitRec xs | acc with (split xs)
69 splitRec xs | acc with (split xs)
@@ -109,7 +109,7 @@ filteredROK p x xs = LTESucc (filterSmaller xs)
109
109
110||| Covering function for the `Filtered` view
110||| Covering function for the `Filtered` view
111||| Constructs the view in O(n lg n)
111||| Constructs the view in O(n lg n)
112−export
112+public export total
113filtered : (p : a -> a -> Bool) -> (xs : List a) -> Filtered p xs
113filtered : (p : a -> a -> Bool) -> (xs : List a) -> Filtered p xs
114filtered p inp with (sizeAccessible inp)
114filtered p inp with (sizeAccessible inp)
115 filtered p [] | _ = FNil
115 filtered p [] | _ = FNil
libs/base/Data/Nat/Views.idr+1−1
@@ -22,7 +22,7 @@ half (S k) with (half k)
22 HalfEven {n=S n}
22 HalfEven {n=S n}
23 half (S (n + n)) | HalfEven = HalfOdd
23 half (S (n + n)) | HalfEven = HalfOdd
24
24
25−export
25+public export total
26halfRec : (n : Nat) -> HalfRec n
26halfRec : (n : Nat) -> HalfRec n
27halfRec n with (sizeAccessible n)
27halfRec n with (sizeAccessible n)
28 halfRec Z | acc = HalfRecZ
28 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
71
71
72||| Covering function for the `SplitRec` view
72||| Covering function for the `SplitRec` view
73||| Constructs the view in O(n lg n)
73||| Constructs the view in O(n lg n)
74−export
74+public export total
75splitRec : (xs : Vect n a) -> SplitRec xs
75splitRec : (xs : Vect n a) -> SplitRec xs
76splitRec {n} input with (sizeAccessible n)
76splitRec {n} input with (sizeAccessible n)
77 splitRec input | acc with (split input)
77 splitRec input | acc with (split input)