Skip to content

Instantly share code, notes, and snippets.

@johannes-riecken

johannes-riecken/vectTake.idr

Created February 22, 2018 01:33
Show Gist options
  • Save johannes-riecken/873740cb8000501ee3d9b76d9eb26dc1 to your computer and use it in GitHub Desktop.
Save johannes-riecken/873740cb8000501ee3d9b76d9eb26dc1 to your computer and use it in GitHub Desktop.
Download ZIP
vectTake implementation
Raw
vectTake.idr
vectTake : (n : Fin (m)) -> Vect m a -> LTE (cast n) m -> Vect (cast n) a
vectTake FZ (y :: xs) LTEZero = []
vectTake (FS y) (z :: xs) (LTESucc x) = z :: vectTake y xs x
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment