[Agda] ANNOUNCE: Agda 2.3.2.2
Sergei Meshveliani
mechvel at botik.ru
Thu Oct 31 11:19:43 CET 2013
On Wed, 2013-10-30 at 17:47 +0100, Nils Anders Danielsson wrote:
> Hi,
>
> Agda 2.3.2.2 has now been released. Important changes since 2.3.2.1:
>
> * Fixed a bug that sometimes made it tricky to use the Emacs mode on
> Windows [issue 757].
>
> * Made Agda build with newer versions of some libraries.
>
In the darcs Agda of August-September 2013 (Alonzo)
the program
odd-suc : ∀ {m} → Even m → Odd (suc m)
odd-suc {0} _ ()
-- no constructor for Even (suc 1)
odd-suc {suc (suc m)} (even+2 even-m) = odd+2 (odd-suc even-m)
is type-checked.
And Agda 2.3.2.2 (Alonzo)
reports
"The number of arguments in the defining equations differ ..."
The version of odd-suc {0} _ = λ ()
is type-checked.
I do not know which checker is better with this respect,
but just point to the difference, for any occasion.
Regards,
------
Sergei
More information about the Agda
mailing list