[Agda] pattern for All is not matched

[Sergei Meshveliani]

On Sun, 2017-01-22 at 10:52 -0800, Martin Stone Davis wrote:
> 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}

Thank you for explanation.
Yes, I have written the thing as

  let es = ...
  in 
  case maximum e es 
  of \
  { (maximum′ m _ (x≤m ∷a xs≤m)) → let a = f m xs≤m
                                   in  foo a
  }

But the corresponding code with one `let' and no `case' looks much more
clear:
  let es                           = ...
      (maximum′ m _ (x≤m ∷a xs≤m)) = maximum e es
      a                            = f m xs≤m
  in  foo a
  
It is a pity that it is not valid. 

------
Sergei


> 
> 
> 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
> 
>