[Agda] Odd behaviour of Agda

[Philip Wadler]

Thanks. Apologies for the repetition. P

On Tue, 7 Aug 2018 at 13:01, Guillaume Allais <guillaume.allais at ens-lyon.org>
wrote:

> 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
> >
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-- 
.   \ 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/20180808/c8ffe6b8/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180808/c8ffe6b8/attachment.ksh>