blob: dc5a224c1b91dc400a5b09087b4bf03e07dba885 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
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)
|
