From 8d58e9d5377cb8821a8d6d274659b5c4cc2a2ed4 Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Thu, 24 Nov 2022 13:40:07 +0000 Subject: refactor: reorder definitions. --- src/Soat/Data/Product.idr | 14 +++++++------- 1 file 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 -- cgit v1.2.3