Idris/advent
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Add listToVect to util

Browse source
This commit is contained in:
Nathan McCarty 2025-02-16 04:03:28 -05:00
parent 5aa490acae
commit 0fc8fa7e18
1 changed files with 8 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/Util.md
View file

@ -192,6 +192,14 @@ Lazily generate all the permutations of a Vect
maxBy f (x :: xs) = Foldable.maxBy f x xs maxBy f (x :: xs) = Foldable.maxBy f x xs
``` ```
### Convert a list to a vect as a sigma type
```idris
export
listToVect : List a -> (n : Nat ** Vect n a)
listToVect xs = (length xs ** fromList xs)
```
## Fin ## Fin
```idris hide ```idris hide