[Agda] Odd behaviour of Agda

[Guillaume Allais]

Hi Phil,

> What is with the extra 1??  How should I file a bug report?

Looks like a time-traveling version of yourself already took care of that:
https://github.com/agda/agda/issues/3002

So it should be fixed in Agda 2.5.4

Cheers!
--
gallais


On 07/08/18 13:36, 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
> 
> 
> .   \ 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/
> 
> 
> 
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
> 
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180807/435032e3/attachment.sig>