[Agda] Termination problems with "with" and recursion

Nils Anders Danielsson nad at cse.gu.se
Mon Dec 2 11:57:27 CET 2013


On 2013-12-02 11:41, Andreas Abel wrote:
>    -- Agda is so stupid,
>    -- cannot even infer the type of this trivial function:
>    plus zero    n = n
>    plus (suc m) n = suc (plus m n)
>    -- What is so difficult about that?  Bitch!

I think this example is a bit strange: plus doesn't have a unique type
(up to definitional equality).

-- 
/NAD


More information about the Agda mailing list