diff options
| author | Greg Brown <greg.brown01@ed.ac.uk> | 2023-07-07 17:36:37 +0100 |
|---|---|---|
| committer | Greg Brown <greg.brown01@ed.ac.uk> | 2023-07-07 17:36:37 +0100 |
| commit | 6b637a6d2954e77985e24bbd17f3697eb6f8238a (patch) | |
| tree | ff60597d324f182084ccf855a25b6f1251034293 /src/Data/Vect/Quantifiers | |
| parent | 8c529393421843a7ccad041d2f29fa90b46bf6b6 (diff) | |
Define properties of substitutions.
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) |