Why does Idris order the arguments to Data.Vect as size then item-type?

Question

Just as the title says. In the other dependent systems I'm familiar with (Agda and Coq), the vector type is defined as Vect : Type -> Nat -> Type. Putting the parameters before the indexes makes sense to me and, in any case, it seems to be the standard for the vector type. Why does Idris use Vect : Nat -> Type -> Type?

Answer 1

There's no observable difference in Idris between parameters and indices. Having the type parameter the last one is convenient for the Functor (Vect n) instance.