diff options
Diffstat (limited to 'src/Data.hs')
| -rw-r--r-- | src/Data.hs | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/Data.hs b/src/Data.hs index a3f4c3c..8c39c6c 100644 --- a/src/Data.hs +++ b/src/Data.hs @@ -52,3 +52,10 @@ deriving instance Traversable (Vec n) vecLength :: Vec n t -> SNat n vecLength VNil = SZ vecLength (_ :< v) = SS (vecLength v) + +vecGenerate :: SNat n -> (forall i. SNat i -> t) -> Vec n t +vecGenerate = \n f -> go n f SZ + where + go :: SNat n -> (forall i. SNat i -> t) -> SNat i' -> Vec n t + go SZ _ _ = VNil + go (SS n) f i = f i :< go n f (SS i) |