<html>
  <head>
    <meta content="text/html; charset=utf-8" http-equiv="Content-Type">
  </head>
  <body bgcolor="#FFFFFF" text="#000000">
    <p>Yeah, it can be somewhat annoying. I proposed an enhancement for
      that <a
        href="https://github.com/agda/agda/issues/2298#issuecomment-263100695">here</a>.</p>
    <br>
    <div class="moz-cite-prefix">On 01/22/2017 11:09 AM, Sergei
      Meshveliani wrote:<br>
    </div>
    <blockquote
      cite="mid:1485112175.2628.14.camel@one.mechvel.pereslavl.ru"
      type="cite">
      <pre wrap="">On Sun, 2017-01-22 at 10:52 -0800, Martin Stone Davis wrote:
</pre>
      <blockquote type="cite">
        <pre wrap="">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}
</pre>
      </blockquote>
      <pre wrap="">
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


</pre>
      <blockquote type="cite">
        <pre wrap="">

On 01/22/2017 10:36 AM, Sergei Meshveliani wrote:
</pre>
        <blockquote type="cite">
          <pre wrap="">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
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
        </blockquote>
        <pre wrap="">

</pre>
      </blockquote>
      <pre wrap="">

</pre>
    </blockquote>
    <br>
  </body>
</html>