vTabulate

vTabulate.agda

vTabulate : {n : Nat}{X : Set} -> (1 <= n -> X) -> Vec X n
vTabulate {zero} f = []
-- _>>_ : {X Y Z : Set} -> (X -> Y) -> (Y -> Z) -> (X -> Z)
-- f : 1 <= suc n -> X
-- f >> g : 1 <= suc n -> Z
-- Q: What would be a useful Z in this case?
-- A: Vec X n
-- So:
-- f >> g : 1 <= suc n -> Vec X n
-- g : X -> Vec X n
-- g == \x -> x _,-_

-- vTabulate {suc n} f = f >> (\ x -> vPure x {suc n}) $ (os oe)
-- vTabulate {suc n} f = f >> (\ x -> x ,- (vPure x)) $ (os oe)

-- X -> Vec X (suc n)
-- 1 <= suc n
vTabulate {suc n} f = (\ p -> f (o' p)) >> {! \ x -> x ,- vTabulate {n} f!}) ( {!!} )

-- vTabulate {suc n} f = {!(f >> (\ x -> x ,- [])) (os oe)!}
-- vTabulate {suc n} f = vPure (f (os (oe {n}))) {suc n}
-- vTabulate {suc n} f = f (os (oe {n})) ,- vTabulate {n} (\ p -> f (o' p))