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