[Agda] lists/vectors

[Dominique Devriese]

Amr,

2012/10/15 Amr Sabry <sabry at cs.indiana.edu>:
> I don't want something of type:
>
>>   (xs : List Bool) -> Vector Bool (length xs)
>
> I really am looking for something of type:
>
>>   (xs : List Bool) -> Vector Bool 32

You could also consider the alternative of making a function of type

  (xs : List Bool) → {_ : ⌊ length xs ≟ 32 ⌋} → Vector Bool 32

where the type "⌊ length xs ≟ 32 ⌋" is constructed to evaluate to ⊤ if
length xs is 32 and to ⊥ if length xs is not equal to 32.

Dominique