[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/

[Guillaume Allais]

Hi Phil,

Post by Philip Wadler
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

Post by 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/
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Philip Wadler]

Thanks. Apologies for the repetition. P

Post by Guillaume Allais
Hi Phil,

Post by Philip Wadler
What is with the extra 1?? How should I file a bug report?

https://github.com/agda/agda/issues/3002
So it should be fixed in Agda 2.5.4
Cheers!
--
gallais

Post by 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/
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Sergei Meshveliani]

Post by 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

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