[Agda] ANNOUNCE: Agda 2.3.2.2

[Nils Anders Danielsson]

On 2013-10-31 11:19, Sergei Meshveliani wrote:
>    "The number of arguments in the defining equations differ ..."

You can find the following information in the draft release notes for
Agda 2.3.4 (which has not been released yet):

* Experimental feature: Varying arity.
   Function clauses may now have different arity, e.g.,

     Sum : ℕ → Set
     Sum 0       = ℕ
     Sum (suc n) = ℕ → Sum n

     sum : (n : ℕ) → ℕ → Sum n
     sum 0       acc   = acc
     sum (suc n) acc m = sum n (m + acc)

   or,

     T : Bool → Set
     T true  = Bool
     T false = Bool → Bool

     f : (b : Bool) → T b
     f false true  = false
     f false false = true
     f true = true

   This feature is experimental.  Yet unsupported:
   * Varying arity and 'with'.
   * Compilation of functions with varying arity to Haskell, JS, or Epic.

-- 
/NAD