How abstraction and application are type-checked [Re: [Agda] Agda type inference oddity on functions]

Nils Anders Danielsson nad at Cs.Nott.AC.UK
Wed Sep 29 00:02:48 CEST 2010


On 2010-09-28 13:43, Alan Jeffrey wrote:
> [...] which looks to me that the order of constraint evaluation is
> making a difference, so constraint solving isn't Church-Rosser!

http://code.google.com/p/agda/issues/detail?id=118

--
/NAD


More information about the Agda mailing list