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

[Jason Dusek]

  With your help, I've managed to produce the much shorter module
  below my signature.

  The interaction between the '\le' shortcut and the letter 'n' is
  most unfortunate.

  This was quite difficult to get sorted; I have no idea where
  `trans' is actually defined for `DecTotalOrder', for example. I
  just read `Relation.Binary' and guessed that I would find `trans'
  where I found `refl'.

  Thank you.

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




module upto where

open import Data.Nat
open import Data.Nat.Properties
open import Relation.Binary
open DecTotalOrder Data.Nat.decTotalOrder using (trans; refl)
open import Data.Fin using (Fin; suc; zero; fromℕ≤)


data Vec (A : Set) : ℕ → Set where
  []  : Vec A zero
  _∷_ : {n : ℕ} → A → Vec A n → Vec A (suc n)

infixl 100 _!_
_!_ : {n : ℕ}{A : Set} → Vec A n → Fin n → A
[]       ! ()
(x ∷ xs) ! zero = x
(x ∷ xs) ! (suc i) = xs ! i


n≤n+1 : {m : ℕ} → m ≤ suc m
n≤n+1 = ≤-step refl

upto : (n : ℕ) → Vec (Fin n) n
upto n = upto' n refl
 where
  upto' : (m : ℕ) → (m ≤ n) → Vec (Fin n) m
  upto' zero m≤n  = []
  upto' (suc m') m≤n = fromℕ≤ m≤n ∷ upto' m' (trans n≤n+1 m≤n)