diff options
| -rw-r--r-- | src/Soat/Data/Product.idr | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/src/Soat/Data/Product.idr b/src/Soat/Data/Product.idr index f92c23c..c4a2acc 100644 --- a/src/Soat/Data/Product.idr +++ b/src/Soat/Data/Product.idr @@ -2,6 +2,7 @@ module Soat.Data.Product import Control.Relation import Data.List.Elem +import Soat.Relation %default total @@ -67,6 +68,23 @@ map f [] = [] map f (x :: xs) = f _ x :: map f xs public export +indexMap : {0 f : IFunc x y} -> (xs : x ^ is) -> (elem : Elem i is) + -> index (map f xs) elem = f i (index xs elem) +indexMap (x :: xs) Here = Refl +indexMap (x :: xs) (There elem) = indexMap xs elem + +public export +mapId : (xs : x ^ is) -> map (\_ => Basics.id) xs = xs +mapId [] = Refl +mapId (x :: xs) = cong ((::) x) $ mapId xs + +public export +mapComp : {0 f : IFunc y z} -> {0 g : IFunc x y} -> (xs : x ^ is) + -> map (\i => f i . g i) xs = map f (map g xs) +mapComp [] = Refl +mapComp (x :: xs) = cong ((::) (f _ (g _ x))) $ mapComp xs + +public export (++) : x ^ is -> x ^ js -> x ^ (is ++ js) (++) [] ys = ys (++) (x :: xs) ys = x :: (xs ++ ys) |