On 2012-02-21 16:27, Brandon Moore wrote: > It seems patterns are always matched left to right. More or less: http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.PatternMatching > Is there any way [...] to have binding occurances inside a dot > pattern? No. -- /NAD