<html><body><div style="color:#000; background-color:#fff; font-family:times new roman, new york, times, serif;font-size:12pt"><div><div><font face="'times new roman', 'new york', times, serif">It seems patterns are always matched left to right.</font></div><div><font face="'times new roman', 'new york', times, serif">Is there any way for matching on patterns more to the right to inform earlier patterns,</font></div><div><font face="'times new roman', 'new york', times, serif">or alternately to have binding occurances inside a dot pattern?</font></div><div><font face="'times new roman', 'new york', times, serif"><br></font></div><div><font face="'times new roman', 'new york', times, serif">Consider this case:</font></div><div><font face="'times new roman', 'new york', times, serif"><br></font></div><div><font face="'times new roman', 'new york', times, serif">module order where</font></div><div><font face="'times new roman', 'new york', times,
serif">open import Data.Bool</font></div><div><font face="'times new roman', 'new york', times, serif"><br></font></div><div><font face="'times new roman', 'new york', times, serif">data Ex : Bool → Set where</font></div><div><font face="'times new roman', 'new york', times, serif"> et : Ex true</font></div><div><font face="'times new roman', 'new york', times, serif"><br></font></div><div><font face="'times new roman', 'new york', times, serif">test : ∀ b → Ex b → Ex b</font></div><div><font face="'times new roman', 'new york', times, serif">test true et = ?</font></div><div><font face="'times new roman', 'new york', times, serif"><br></font></div><div><font face="'times new roman', 'new york', times, serif">In the cases where this bothers me, the later pattern takes implicit arguments, and I'd rather write</font></div><div><font face="'times new roman', 'new york', times, serif">something like</font></div><div><font face="'times new
roman', 'new york', times, serif"><br></font></div><div><font face="'times new roman', 'new york', times, serif">fun (l $ r) (a $$ b) = ...</font></div><div><font face="'times new roman', 'new york', times, serif"><br></font></div><div><font face="'times new roman', 'new york', times, serif">rather than</font></div><div><font face="'times new roman', 'new york', times, serif"><br></font></div><div><font face="'times new roman', 'new york', times, serif">fun .(l $ r) (_$$_ {l = l} {r} a b) = ...</font></div><div><font face="'times new roman', 'new york', times, serif"><br></font></div><div><font face="'times new roman', 'new york', times, serif">Another idea is maybe to have some kind of antiquote inside dot patterns -</font></div><div><font face="'times new roman', 'new york', times, serif">read</font></div><div><font face="'times new roman', 'new york', times, serif">fun .(,l $ ,r) (a $$ b)</font></div><div><font face="'times new roman', 'new york',
times, serif">as something like "based on later arguments you should be able to tell that the</font></div><div><font face="'times new roman', 'new york', times, serif">top level constructor of the first argument is _$_, and then bind l and r to the</font></div><div><font face="'times new roman', 'new york', times, serif">subterms (which can be assembled from implicit parameters of later arguments).</font></div><div><font face="'times new roman', 'new york', times, serif"><br></font></div><div><font face="'times new roman', 'new york', times, serif">Brandon</font></div></div></div></body></html>