[Agda] pattern for All is not matched

[Martin Stone Davis]

Let bindings don't let you match against "datatype patterns", only 
record patterns. _∷a_ is a datatype pattern in this sense (List being a 
datatype, after all). For datatypes, you can use case_of_:

open import Function

f :  (x m : ℕ) → (xs : List ℕ) → All (_≤ m) (x ∷ xs) → x ≤ m
f x m xs xxs≤m =
                case xxs≤m of λ {(x≤m ∷a xs≤m) → x≤m}


On 01/22/2017 10:36 AM, Sergei Meshveliani wrote:
> Please, why matching against  (x≤m ∷a xs≤m)
> is not type-checked below?
>
> For the program
>
> -----------------------------------------------
> open import Data.Nat  using (ℕ; _≤_)
> open import Data.List using (List; _∷_)
> open import Data.List.All as AllM using (All)
>                                    renaming (_∷_ to _∷a_)
>
> f :  (x m : ℕ) → (xs : List ℕ) → All (_≤ m) (x ∷ xs) → x ≤ m
> f x m xs xxs≤m =
>                 let  (x≤m ∷a xs≤m) = xxs≤m  in  x≤m
> --------------------------------------------------
>
> Agda 2.5.2 reports
>
>    Expected record pattern
>    when checking the let binding x≤m ∷a xs≤m = xxs≤m
>
> In what place does it expect a record?
> Is this a bug in Agda ?
>
> The variant of
>
>      f x m xs (x≤m ∷a xs≤m) = x≤m
>
> is type-checked.
>
>
> In reality, I need to use the pattern like
>     
>    let (maximum′ m _ (x≤m ∷a xs≤m)) = maximum x xs
>    in
>    foo m x≤m xs≤m,
>
> where maximum′ is the constructor for the result record for the
> `maximum' function.
> Matching against
>                  (maximum′ m _ _)
>   
> is type-checked under this `let', while matching against
> (maximum′ m _ (x≤m ∷a xs≤m))
> is not
> (again, "Expected record pattern").
>
> Thanks,
>
> ------
> Sergei
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda