[Agda] Pattern matching order?

[Brandon Moore]

It seems patterns are always matched left to right.
Is there any way for matching on patterns more to the right to inform earlier patterns,
or alternately to have binding occurances inside a dot pattern?

Consider this case:

module order where
open import Data.Bool

data Ex : Bool → Set where
  et : Ex true

test : ∀ b → Ex b → Ex b
test true et = ?

In the cases where this bothers me, the later pattern takes implicit arguments, and I'd rather write
something like

fun (l $ r) (a $$ b) = ...

rather than

fun .(l $ r) (_$$_ {l = l} {r} a b) = ...

Another idea is maybe to have some kind of antiquote inside dot patterns -
read
fun .(,l $ ,r) (a $$ b)
as something like "based on later arguments you should be able to tell that the
top level constructor of the first argument is _$_, and then bind l and r to the
subterms (which can be assembled from implicit parameters of later arguments).

Brandon
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20120221/ce5f43b5/attachment.html