[Agda] Odd behaviour of Agda

[Philip Wadler]

If I write the code

\begin{code}
_≤??_ : ∀ (m n : ℕ) → Dec (m ≤ n)
zero  ≤?? n                   =  yes z≤n
suc m ≤?? zero                =  no λ()
suc m ≤?? suc n with m ≤?? n
...               | yes m≤n  =  yes (s≤s m≤n)
...               | no ¬m≤n  =  no λ{ (s≤s m≤n) → ¬m≤n m≤n }
\end{code}

and execute

2 ≤?? 4

then I get the answer

no (λ { (s≤s m≤n) → (λ { (s≤s m≤n) → (λ ()) 1 m≤n }) m≤n })

What is with the extra 1??  How should I file a bug report? Cheers, -- P


.   \ Philip Wadler, Professor of Theoretical Computer Science,
.   /\ School of Informatics, University of Edinburgh
.  /  \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/

Too brief? Here's why: http://www.emailcharter.org/
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180807/a6b817c4/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180807/a6b817c4/attachment.ksh>