[Agda] Agda2 beginner's question

[kahl at cas.mcmaster.ca]

 > 
 > On 2009-11-30 13:36, kahl at cas.mcmaster.ca wrote:
 > > Afterthought: Can agda-mode help me to fill in ``.({! !})'' automatically?
 > 
 > If you mean .e rather than .?, then yes. Try using case-split (C-c C-c).
 > 
 > --
 > /NAD

So I am now trying to start with:


module Matrix where

open import Data.Nat
open import Data.Vec
open import Data.Fin using (toℕ)

Matrix : Set → ℕ → ℕ → Set
Matrix A m n = Vec (Vec A n) m

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



Hitting C-c C-c inside the goal, the minibuffer prompts me:

  partten var to case:  

(should ``partten'' be ``pattern''?)

and apparently no matter what I type in, I always get *Error*:

  Right hand side must be a single hole when making a case
  distinction.
  when checking that the expression ? has type
  Vec (Data.Fin.Fin (m * n)) (m * n)

I also get this when I replace the part after ``='' with another hole,
trying to satisfy ``Right hand side must be a single hole''.

I suspect I didn't understand your instructions (nor the error message) ---
what should I do to have case-split help me?


Wolfram