[Agda] lists/vectors

[Dominique Devriese]

Amr,

2012/10/15 Amr Sabry <sabry at cs.indiana.edu>:
> I hope you don't mind the personal email.

I don't mind, but if a question or answer could be useful for other
people as well, I prefer to send it to the list.

> This is helpful and I've tried
> to do something along these lines. I hope you don't mind one more question:
>
>>   (xs : List Bool) → {_ : ⌊ length xs ≟ 32 ⌋} → Vector Bool 32
>
> What's the type of ⌊_⌋
>
> In Relation.Nullary.Decidable, we have:
>
> ⌊_⌋ : ∀ {p} {P : Set p} → Dec P → Bool
>
> but that can't possibly what you mean. Did you perhaps mean:
>
> True : ∀ {p} {P : Set p} → Dec P → Set

You are right, I meant True instead of  ⌊_⌋. Teaches me to type-check
suggestions before sending them ;).

While you're looking in the library, consider the _div_ function in
Data.Nat.DivMod for inspiration. I think Ulf Norell documents the
pattern somewhere in his PhD thesis if you want more background.

Dominique