idris-lang/Idris-dev — pull request #977 by jedesah (2014-03-18 04:17:54+00:00)
Title: Add length to Vect

I thought it would be useful to add the length function to Vect as well.

Motivation:

indexAsString <- getLine
let indexAsInt : Integer = cast indexAsString
let items: Vect _ _ = ["shoe", "bat", "hat"]
let i = integerToFin indexAsInt $ length items
maybe (print "invalid index") (\ii => print $ index ii items) i

Is there something I am missing? Some better way to express this without requiring the length function to be defined on Vect.

Also, the implementation is very basic. I tried to figure out a way to express the fact that length is already known through the type and that we should not have to "re-calculate" it but failed.