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