[Agda] Unification of function types
Nils Anders Danielsson
nad at cse.gu.se
Thu Sep 19 16:43:28 CEST 2013
On 2013-09-19 16:18, Jesper Cockx wrote:
> I guess the problem with the first definition is that Agda doesn't
> know how to unify the two types (x : A₁) → B₁ x and (x : A₁) → B₂ x.
> Would it be problematic add such a rule to the unification algorithm?
You may be interested in the following mailing list threads:
Agda with the excluded middle is inconsistent ?
More information about the Agda