[Agda] Influencing pattern matching order [Was: Absurd pattern; convincing Agda]

[Nils Anders Danielsson]

On 2012-06-12 15:50, Dominique Devriese wrote:
> One solution that I have used before is the following. You can
> influence the order of the pattern matches that Agda will compile your
> outerIsEq function to by adding fake "with" pattern matches on known
> values:
>
>    outerIsEq (def f args) with Data.Nat._≟_ (length args) 4
>    outerIsEq (def f args) | yes p with tt

Perhaps the following approach would also work (untested):

   outerIsEq (def f args) with Data.Nat._≟_ (length args) 4 | args
   outerIsEq (def f args) | yes p | [] = …
   ⋮

-- 
/NAD