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