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

[Conor McBride]

Hi folks

I meant to send this to the list.

Brain damage

Conor

Begin forwarded message:

> From: Conor McBride <conor at strictlypositive.org>
> Date: 18 February 2011 08:49:29 GMT
> To: Jason Dusek <jason.dusek at gmail.com>
> Subject: Re: [Agda] how to count 0..n-1
>
> Hi Jason
>
> On 18 Feb 2011, at 01:13, Jason Dusek wrote:
>
>> With your help, I've managed to produce the much shorter module
>> below my signature.
>
>> 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
>
> This is a good start. I recommend to invert !, writing
>
>  tabulate : forall {n X} -> (Fin n -> X) -> Vec X n
>
> and then yer upto is an easy special case. I'd say more,
> but I set it as an exercise in my Agda course.
>
> Cheers
>
> Conor
>
>
>>
>>
>> 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)
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>