From 6b637a6d2954e77985e24bbd17f3697eb6f8238a Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Fri, 7 Jul 2023 17:36:37 +0100
Subject: Define properties of substitutions.

---
 src/Data/Vect/Quantifiers/Extra.idr | 14 ++++++++++++++
 1 file changed, 14 insertions(+)
 create mode 100644 src/Data/Vect/Quantifiers/Extra.idr

(limited to 'src/Data/Vect')

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)
-- 
cgit v1.2.3