[Agda] matching against _::_ ?

[Andreas Abel]

You can use vectors:

open import Data.Nat.Base
open import Data.Vec
open import Function

test : ℕ
test = case 1 ∷ 2 ∷ 3 ∷ [] of λ where
   (a ∷ b ∷ c ∷ _) → a + b + c


On 07.06.2017 22:03, Sergei Meshveliani wrote:
> People,
> 
> I have a function of kind
> 
>    let a = gen 1
>        b = gen 2
>        c = gen 3
>        d = gen 4
>        e = gen 5
>        f = gen 6
>        g = gen 7
>    in
>    F a b (c d) (H e f g)
> 
> And in other examples there may be more `gen' values of this kind.
> 
> Is it possible a shorter expression?
> 
> For the construct of kind
> 
>    let  a ∷ b ∷ c ∷ _ =  gen 1 ∷ gen 2 ∷ gen 3 ∷ []
>    in   ...
> 
> Agda reports  "Expected record pattern ...".
> Why?
> 
> And with
>     case gen 1 ∷ gen 2 ∷ gen 3 ∷ []
>     of
>     { (a ∷ b ∷ c ∷ _) → a + b + c
>     ; _               → ??
>     },
> 
> I do not see how to eliminate the remaining patterns in a short code.
> 
> How to make Agda accept that the list  gen 1 ∷ gen 2 ∷ gen 3 ∷ []
> has at least three members, and to pattern-match accordingly?
> 
> What may be a way out?
> 
> Thanks,
> 
> ------
> Sergei
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www.cse.chalmers.se/~abela/