<div dir="ltr">If I write the code<div><br></div><div><div>\begin{code}</div><div>_≤??_ : ∀ (m n : ℕ) → Dec (m ≤ n)</div><div>zero  ≤?? n                   =  yes z≤n</div><div>suc m ≤?? zero                =  no λ()</div><div>suc m ≤?? suc n with m ≤?? n</div><div>...               | yes m≤n  =  yes (s≤s m≤n)</div><div>...               | no ¬m≤n  =  no λ{ (s≤s m≤n) → ¬m≤n m≤n }</div><div>\end{code}</div><div><br></div><div>and execute</div><div><br></div><div>2 <span style="font-size:small;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline">≤?? 4</span></div><div><span style="font-size:small;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline"><br></span></div><div><span style="font-size:small;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline">then I get the answer</span></div><div><span style="font-size:small;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline"><br></span></div><div><span style="background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline">no (λ { (s≤s m≤n) → (λ { (s≤s m≤n) → (λ ()) 1 m≤n }) m≤n })<br></span></div><div><br></div><div><span style="background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline">What is with the extra 1??  How should I file a bug report? Cheers, -- P</span></div><div><span style="background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline"><br></span></div><div><span style="background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline"><br></span></div><div><div class="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></div>
</div></div>