Skip to content

Instantly share code, notes, and snippets.

@hughfdjackson

hughfdjackson/least-effecient-reverse.idr

Created September 29, 2014 15:04
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save hughfdjackson/7a34d3cac5cd22149e90 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save hughfdjackson/7a34d3cac5cd22149e90 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
least-effecient-reverse.idr
module reverse
total snoc : Vect n a -> a -> Vect (S n) a
snoc Nil a = a :: Nil
snoc (x :: xs) a = x :: (xs `snoc` a)
total reverse' : Vect n a -> Vect n a
reverse' (x :: xs) = (reverse' xs) `snoc` x
reverse' Nil = Nil
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment