[Agda] Agda2 beginner's question

[Nils Anders Danielsson]

On 2009-11-30 02:40, kahl at cas.mcmaster.ca wrote:
>  > unconcat' : ∀ {a n k} {xs : Vec  a (n * k)} → Group n k xs → Vec (Vec a k) n
>  > unconcat' (concat' xss) = xss
>  >
>  > group' : ∀ {a} n k (xs : Vec a (n * k)) → Vec (Vec a k) n
>  > group' n k xs = unconcat' (group n k xs)
>
> (Would those be candidates for inclusion in the standard library?)

I switched to a variant of group which uses an explicit equality proof:

  group : ∀ {A} n k (xs : Vec A (n * k)) →
          ∃ λ (xss : Vec (Vec A k) n) → xs ≡ concat xss

--
/NAD


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.