[Agda] matching against _::_ ?

[Sergei Meshveliani]

On Fri, 2017-06-09 at 09:49 +0200, Sandro Stucki wrote:
[..]

> I'm not sure I understand your question correctly, but if you're just
> trying collect multiple let-definitions in one line, using products
> instead of vectors/lists might help:
> 
> -------------------------------------------------------------------
> -- ...
> open import Data.Product using (_,_; _,′_)
> 
> -- ...
> test2 : (a b c : ℕ) → (a + b) + c ≡ a + (b + c)
> test2 a b c =
>             let a' , b' , c' = suc a ,′ suc b ,′ suc c
> 
>                 eq :  (a' + b') + c' ≡ a' + (b' + c')
>                 eq =  +-assoc a' b' c'
>             in
>             suc-assoc a b c eq
> -------------------------------------------------------------------
> 
> You can avoid the use of _,′_ by defining your own (non-dependent) product type.



Thanks to Sandro and to Andreas.

Now I see a way out.
The goal was to write shorter the assignments of kind

  :a-0 = gen 0,      
  ...                                       
  :a-n = gen n                                                 

for certain    gen : Nat -> Expr,   and n being, say, up to 20.
Now, I define

module _ {α} (A : Set α)
  where
  Tuple1 :  {n : ℕ} → Set α
  Tuple1 {0}     =  A
  Tuple1 {suc n} =  A × (Tuple1 {n})

  seqInTuple1 :  (ℕ → A) → (n : ℕ) → Tuple1 {n},


so that,  (seqInTuple f n)  returns  
                            (f 0 , f 1 , ... , f n) :  Tuple1 {n}.

And apply it as in this example:

 :g₁₂ , :g₂₃ , :pN , :pD , :p'N , :p'D , :pG , :p'G =
                                               seqInTuple1 Expr gen 7

Thanks,

------
Sergei