module Data.Vect.Quantifiers.Extra

import Data.Vect
import Data.Vect.Quantifiers

export
mapRel : ((x : a) -> p x -> q x) -> {xs : Vect n a} -> All p xs -> All q xs
mapRel f [] = []
mapRel f (px :: pxs) = f _ px :: mapRel f pxs

export
tabulate : {n : Nat} -> (0 f : Fin n -> a) -> ((i : Fin n) -> p (f i)) -> All p (tabulate f)
tabulate {n = 0} f pf = []
tabulate {n = S k} f pf = pf FZ :: tabulate (f . FS) (\i => pf $ FS i)