[Agda] Pattern-matching operation order

[Ulf Norell]

2010/2/19 Andreas Abel <andreas.abel at ifi.lmu.de>

>
> The connection of our problem to the one in the thread is not apparent.
>  Here is a rephrasement of the problem, not using dot patterns.
>
> f : {n m : Nat} -> D n (suc m) -> Nat
> f (c (suc i) zero) = bla              -- FAILS already
> f (c i (suc zero)) = bla
> f (c zero zero)
>

> How would I write a series of patterns for f that do type-check?


Here's how you do it:

f′ : {n m′ m : Nat} -> D n m′ -> m′ ≡ suc m -> Nat
f′ (c (suc i) zero) refl = bla
f′ (c i (suc zero)) refl = bla
f′ (c i (suc (suc d))) refl = {!you missed this case!}
f′ (c zero zero) ()

f : {n m : Nat} -> D n (suc m) -> Nat
f d = f′ d refl

The reason your version is not accepted is that the type checking algorithm
requires that each function definition corresponds to a (type correct) case
splitting tree. Basically, if you can't C-c C-c your way to the definition
it won't be accepted. In your example

  f (c i d) = ?

is not a valid refinement of the problem f x = ? (since d + i doesn't unify
with suc m).

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20100219/aedfa787/attachment.html