[Agda] how to count 0..n-1

[Nils Anders Danielsson]

On 2011-02-05 09:55, Jason Dusek wrote:
>    Now, I think this is because `upto m' has type `Fin m' and
>    not `Fin n'. Do I need an additional, perhaps implicit
>    parameter? Perhaps a proof term?

You could use weakening. See Data.Vec.allFin in the standard library.

-- 
/NAD