[Agda] Agda2 beginner's question

[Andreas Abel]

After some fresh air more parts of my brain have started working  
again, only for a short time I think, but it was enough to locate the  
actual source of the failure.

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

Thus, no need to change the standard library.  To match "group m n v"  
you also need to match v which is forced to be "concat xss" (dot  
pattern).  Agda refuses to see that  concat xss = v until you rub her  
nose in it.

This trick is already used in the definition of group, that's where I  
stole it from.

Cheers,
Andreas

On Nov 25, 2009, at 4:37 AM, kahl at cas.mcmaster.ca wrote:

> Dear Agda list,
>
>  I know Haskell, including GADTs, and have used Isabelle before;
> now I am just starting to try to get going with Agda2
> and hit a serious roadblock in trying to unwrap a Data.Vec.Group
> from the standard library (lib-0.2) to get at the enclosed Vec  
> (Vec ...).
>
> Since my ``group'' application appears to type check,
> I would not have expected to be asked to prove
>
>  concat xss = allFin (n * m)
>
> before I can bind ``xss'' in the concat' pattern.
> And even if I really have to do it, I have no idea how to start...
>
>
> What am I overlooking?
>
>
> Wolfram
>
>
> ----
> module Matrix where
>
> open import Data.Nat
> open import Data.Vec
> open import Data.Function using (_$_)
> open import Data.Fin using (toℕ)
>
> Matrix : Set → ℕ → ℕ → Set
> Matrix A m n = Vec (Vec A n) m
>
>
> transpose : ∀ {A m n} → Matrix A m n → Matrix A n m
> transpose [] = replicate []
> transpose (xs ∷ xss) = zipWith _∷_ xs (transpose xss)
>
>
> mat1 : (m : ℕ) → (n : ℕ) → Matrix ℕ m n
> mat1 m n with group n m (allFin (n * m))
> mat1 m n | concat' xss  = map (map toℕ) xss
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

Andreas ABEL
INRIA, Projet Pi.R2
23, avenue d'Italie
F-75013 Paris
Tel: +33.1.39.63.59.41