diff options
Diffstat (limited to 'src/Data/Vect/Quantifiers')
| -rw-r--r-- | src/Data/Vect/Quantifiers/Extra.idr | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/src/Data/Vect/Quantifiers/Extra.idr b/src/Data/Vect/Quantifiers/Extra.idr new file mode 100644 index 0000000..dc5a224 --- /dev/null +++ b/src/Data/Vect/Quantifiers/Extra.idr @@ -0,0 +1,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) |