Noratrieb/idris-learning
1
0
Fork 0
mirror of https://github.com/Noratrieb/idris-learning.git synced 2026-01-15 21:45:01 +01:00
Code Issues Projects Releases Packages Wiki Activity Actions

chapter 3 finished

Browse source
This commit is contained in:
nora 2021-07-09 11:36:37 +02:00
parent c43a16ecde
commit 9c41b5059e
2 changed files with 39 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

9
chapter3/Vectors.idr
View file

@ -52,3 +52,12 @@ my_map f (x :: xs) = (f x) :: my_map f xs
my_vect_map : (a -> b) -> Vect n a -> Vect n b
my_vect_map _ [] = []
my_vect_map f (x :: xs) = (f x) :: my_vect_map f xs
lengthLong : Vect n elem -> Nat
lengthLong [] = 0
lengthLong (x :: xs) = S (lengthLong xs)
lengthLong2 : Vect n elem -> Nat
lengthLong2 {n} xs = n