diff options
Diffstat (limited to 'src/Soat/Data')
| -rw-r--r-- | src/Soat/Data/Product.idr | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/src/Soat/Data/Product.idr b/src/Soat/Data/Product.idr index 4604300..c5cebe4 100644 --- a/src/Soat/Data/Product.idr +++ b/src/Soat/Data/Product.idr @@ -27,13 +27,6 @@ uncurry : map x is `ary` a -> x ^ is -> a uncurry f [] = f uncurry f (x :: xs) = uncurry (f x) xs --- Constructors - -public export -tabulate : {is : List a} -> ({i : a} -> Elem i is -> x i) -> x ^ is -tabulate {is = []} f = [] -tabulate {is = (i :: is)} f = f Here :: tabulate (f . There) - -- Destructors public export @@ -53,6 +46,13 @@ index : x ^ is -> Elem i is -> x i index xs Here = head xs index xs (There elem) = index (tail xs) elem +-- Constructors + +public export +tabulate : {is : List a} -> ({i : a} -> Elem i is -> x i) -> x ^ is +tabulate {is = []} f = [] +tabulate {is = (i :: is)} f = f Here :: tabulate (f . There) + -- Operations public export |