[Agda] pattern for All is not matched

[Martin Stone Davis]

Yeah, it can be somewhat annoying. I proposed an enhancement for that 
here <https://github.com/agda/agda/issues/2298#issuecomment-263100695>.


On 01/22/2017 11:09 AM, Sergei Meshveliani wrote:
> 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
>>
>

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170122/7b209668/attachment.html>