[Agda] Agda2 beginner's question

[Julian Beaumont]

On Tue, Dec 1, 2009 at 12:59 AM,  <kahl at cas.mcmaster.ca> wrote:
>  >
>  > 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
>

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.

Julian.