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

[Jason Dusek]

  I am trying to write a simple program that counts from
  zero to pred n:

    upto : (n : ℕ) → Vec (Fin n) n
    upto n with n
    ... | zero  = []
    ... | suc m = fromℕ m ∷ upto m

  However, I get a type error:

    /home/solidsnack/sandbox/agda-tutorial/exercize_2-1.agda:35,25-31
    m != suc m of type ℕ
    when checking that the expression upto m has type
    Vec (Fin (suc m)) (_102 n m)

  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?

--
Jason Dusek
Linux User #510144 | http://counter.li.org/