[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