[Agda] Agda2 beginner's question

[kahl at cas.mcmaster.ca]

Julian,

 > You should start with
 > 
 > 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 | v | g = {! !}
 > 
 > Hitting C-c C-c and entering g as the pattern variable should replace
 > g with the concat' and fill in the appropriate dot-pattern for v.

Thank you!  That works!
(I had not such expected ``side effects'' of goal manipulation.)



Wolfram