<div><div dir="auto">Thanks. Apologies for the repetition. P</div></div><div><br><div class="gmail_quote"><div dir="ltr">On Tue, 7 Aug 2018 at 13:01, Guillaume Allais <<a href="mailto:guillaume.allais@ens-lyon.org">guillaume.allais@ens-lyon.org</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Phil,<br>
<br>
> What is with the extra 1??  How should I file a bug report?<br>
<br>
Looks like a time-traveling version of yourself already took care of that:<br>
<a href="https://github.com/agda/agda/issues/3002" rel="noreferrer" target="_blank">https://github.com/agda/agda/issues/3002</a><br>
<br>
So it should be fixed in Agda 2.5.4<br>
<br>
Cheers!<br>
--<br>
gallais<br>
<br>
<br>
On 07/08/18 13:36, Philip Wadler wrote:<br>
> If I write the code<br>
> <br>
> \begin{code}<br>
> _≤??_ : ∀ (m n : ℕ) → Dec (m ≤ n)<br>
> zero  ≤?? n                   =  yes z≤n<br>
> suc m ≤?? zero                =  no λ()<br>
> suc m ≤?? suc n with m ≤?? n<br>
> ...               | yes m≤n  =  yes (s≤s m≤n)<br>
> ...               | no ¬m≤n  =  no λ{ (s≤s m≤n) → ¬m≤n m≤n }<br>
> \end{code}<br>
> <br>
> and execute<br>
> <br>
> 2 ≤?? 4<br>
> <br>
> then I get the answer<br>
> <br>
> no (λ { (s≤s m≤n) → (λ { (s≤s m≤n) → (λ ()) 1 m≤n }) m≤n })<br>
> <br>
> What is with the extra 1??  How should I file a bug report? Cheers, -- P<br>
> <br>
> <br>
> .   \ Philip Wadler, Professor of Theoretical Computer Science,<br>
> .   /\ School of Informatics, University of Edinburgh<br>
> .  /  \ and Senior Research Fellow, IOHK<br>
> . <a href="http://homepages.inf.ed.ac.uk/wadler/" rel="noreferrer" target="_blank">http://homepages.inf.ed.ac.uk/wadler/</a><br>
> <br>
> Too brief? Here's why: <a href="http://www.emailcharter.org/" rel="noreferrer" target="_blank">http://www.emailcharter.org/</a><br>
> <br>
> <br>
> <br>
> The University of Edinburgh is a charitable body, registered in<br>
> Scotland, with registration number SC005336.<br>
> <br>
> <br>
> <br>
> _______________________________________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
> <br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div></div>-- <br><div dir="ltr" class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr">.   \ Philip Wadler, Professor of Theoretical Computer Science,<br>.   /\ School of Informatics, University of Edinburgh<br></div><div>.  /  \ and Senior Research Fellow, IOHK<br></div><div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/wadler/</a></span></div></div><div dir="ltr"><br></div><div>Too brief? Here's why: <a href="http://www.emailcharter.org/" target="_blank">http://www.emailcharter.org/</a></div></div></div></div></div>