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

[gallais at EnsL.org]

I was working on vectors lately (in Coq but that's not important here) and I
was quite unsatisfied both with what my map function was able to do and
with the way allFin was defined in my development.

I ended up defining a more powerful map function which is actually quite
convenient (not only to define allFin) and which is able to generate allFin
more efficiently.

If anyone is interested (I dit not bother to add levels but I guess
that it would
be needed if one wanted the code to be as generic as possible), here is the
translation of my code in Agda:

=================================

module Fin_vec where

import Data.Nat as ℕ
open import Data.Fin
open import Data.Vec

Vmapfull : ∀ {A B : Set} {n} (f : ∀ (p : Fin n) → A → B) (v : Vec A n) → Vec B n
Vmapfull f [] = []
Vmapfull f (x ∷ xs) = (f zero x) ∷ (Vmapfull (λ p → f (suc p)) xs)

MakeVec : ∀ {A : Set} n (a : A) → Vec A n
MakeVec ℕ.zero a = []
MakeVec (ℕ.suc n) a = a ∷ MakeVec n a

allFin′ : ∀ n → Vec (Fin n) n
allFin′ n = Vmapfull (λ p _ → p) (MakeVec _ ℕ.zero)

=================================

Cheers,

--
guillaume



On 11 February 2011 13:16, Nils Anders Danielsson <nad at chalmers.se> wrote:
> I tend not to worry too much about inefficiency when working with unary
> numbers. Note, however, that allFin n has a size which is quadratic in
> the size of n, so unless we make use of sharing we cannot hope for
> better than quadratic complexity.