idris-lang/Idris-dev — pull request #980 by david-christiansen (2014-03-18 13:43:45+00:00)
Title: Add some vector docs

This includes #977, but it specifies when Vect.length should be applied (ie seldom).