From e3747417cdb6e5d24caf4af4cc18d5fd9348a103 Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Thu, 24 Nov 2022 13:41:18 +0000 Subject: Prove relationship between index and tabulate. --- src/Soat/Data/Product.idr | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'src') diff --git a/src/Soat/Data/Product.idr b/src/Soat/Data/Product.idr index c5cebe4..e9c3d17 100644 --- a/src/Soat/Data/Product.idr +++ b/src/Soat/Data/Product.idr @@ -53,6 +53,12 @@ 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) +public export +indexTabulate : forall x . (0 f : {i : a} -> Elem i is -> x i) -> (elem : Elem i is) + -> index (tabulate f) elem = f elem +indexTabulate f Here = Refl +indexTabulate f (There elem) = indexTabulate (f . There) elem + -- Operations public export -- cgit v1.2.3