Skip to content

Instantly share code, notes, and snippets.

@hughfdjackson

hughfdjackson/concat.idr

Last active August 29, 2015 14:07
Show Gist options

  • Select an option

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

Select an option

Learn more about clone URLs
Save hughfdjackson/756ab2ec7ebf1a3f94b2 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
concat.idr
sPlusAssoc : (m, n: Nat) -> S (m + n) = plus m (S n)
sPlusAssoc Z n = refl
sPlusAssoc (S m) n = rewrite sPlusAssoc m n in refl
total concat : Vect n a -> Vect m a -> Vect ((replace sPlusAssoc) (plus m n)) a
concat (x :: xs) ys = x :: (concat xs ys)
concat nil ys = ys
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment