[Agda] Agda2 beginner's question

[kahl at cas.mcmaster.ca]

First of all, thanks to Andreas Abel, who solved my problem of not
being able to unwrap the concat' from the group result:

 > It is some "magic with" sorcery which makes your example work.
 > 
 > mat1 : (m : ℕ) → (n : ℕ) → Matrix ℕ m n
 > mat1 m n with allFin (m * n)
 > mat1 m n | v  with group m n v
 > mat1 m n | .(concat xss) | concat' xss  = map (map toℕ) xss

Also thanks to Nils Anders Danielsson for the detailed explanations he
gave, and to Nicolas Pouillard for showing me that I could just have
defined the inverse of concat' myself:

 > 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?)

With that, my definition becomes trivial:

mat2 : (m : ℕ) → (n : ℕ) → Matrix ℕ m n
mat2 m n = map (map toℕ) (group' m n (allFin (m * n)))


Looking at Andreas' version, I suspected that my previous impression
that .-arguments could always be replaced with wildcards was wrong,
so I tried it out:

mat1 : (m : ℕ) → (n : ℕ) → Matrix ℕ m n
mat1 m n with allFin (m * n)
mat1 m n | v  with group m n v
mat1 m n | ._    | concat' xss  = map (map toℕ) xss

This actually works (and it does not work without the dot).
Does writing ``.(e)'' for some expression e ever make a difference over
writing ``._'' (except for documentation, of course)?



Thanks a lot for the warm welcome!  :-)


Wolfram