Add function "vZip" to SAWCore prelude and set up for evaluator

GaloisInc · May 28, 2014 · 1f75778 · 1f75778
1 parent ecfa781
commit 1f75778
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/prelude/Prelude.sawcore b/prelude/Prelude.sawcore
@@ -614,6 +614,9 @@ rotateL :: (n :: Nat) -> (a :: sort 0) -> Vec n a -> Nat -> Vec n a;
 -- Rotate array to the right.
 rotateR :: (n :: Nat) -> (a :: sort 0) -> Vec n a -> Nat -> Vec n a;
 
+-- Zip together two lists (truncating the longer of the two).
+vZip :: (a b :: sort 0) -> (m n :: Nat) -> Vec m a -> Vec n b -> Vec (minNat m n) #(a, b);
+
 --------------------------------------------------------------------------------
 -- Bitvectors