Skip to content

Instantly share code, notes, and snippets.

@expede

expede/VecConcat.idr

Last active October 21, 2016 15:16
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save expede/a1e60c3041bf5aeeb1d6f0198e0579e8 to your computer and use it in GitHub Desktop.
Save expede/a1e60c3041bf5aeeb1d6f0198e0579e8 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
VecConcat.idr
{-
Vectors are fixed-length data structures
They're written in this format: `Vect length type`
ex. `Vect 3 Int` could represent [1,2,3], but not [1,2] or ['a', 'b', 'c']
-}
concat : Vect lengthX a -> Vect lengthY a -> Vect (lengthX + lengthY) a
concat Nil ys = ys
concat (x :: xs) ys = x :: app xs ys
-- ie: take the lengths of two vetcors,
-- and the result must have the length of the two combined
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment