diff options
| author | Tom Smeding <t.j.smeding@uu.nl> | 2024-09-03 17:00:08 +0200 |
|---|---|---|
| committer | Tom Smeding <t.j.smeding@uu.nl> | 2024-09-03 17:00:08 +0200 |
| commit | 40a6868ed5960d381359541975272483747808b4 (patch) | |
| tree | aeda3bdf22bd3fef5366b37cb78b5cbf8c7018c7 /src/Data.hs | |
| parent | e281439863d7e760a60b573f53604aac5e737984 (diff) | |
Inching towards drev of build
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) |