idris-lang/Idris-dev — pull request #1272 by jeffersoncarpenter (2014-05-31 01:41:21+00:00)
Title: added insertAt function to Vect

how's the last case, style-wise?