[Agda] Odd behaviour of Agda

[Sergei Meshveliani]

On Tue, 2018-08-07 at 12:36 +0100, Philip Wadler wrote:
> 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


In Agda 2.5.4,  I command in the interactive mode  C-u C-c C-n  and
obtain
   2 ≤?? 4
   yes (s≤s (s≤s z≤n))

The code is 

-------------------------------------------------
open import Relation.Nullary using (Dec; yes; no)
open import Data.Nat using (ℕ; _≤_)
open ℕ
open _≤_

_≤??_ : ∀ (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 }
-------------------------------------------------

--
SP