idris-lang/Idris-dev — pull request #691 by sjdrodge (2013-11-29 22:13:29+00:00)
Title: Some Prelude cleanup (Fin and Vect)

I've changed the type signatures of finToNat, Vect.take, and Vect.drop. I've also renamed finToInt to the more accurate finToInteger and changed its type signature in the process.

I also added two proof helpers to Prelude.Fin: FinZAbsurd and FinZElim.