[Agda] exhaustive patterns

[Andreas Abel]

The reason you cannot replace 'nothing' with an underscore '_' is that 
Agda first checks that each individual clause is well-typed, and only 
then does a coverage check which would reveal that '_' must actually be 
'nothing'.

Since '_' is just a variable, the emptyness check fails, which succeeds 
with the more informative 'nothing'.

Does this help?

Cheers,
Andreas


Am 18.02.2013 18:06, schrieb Serge D. Mechveliani:
> Dear all,
>
> I have a question about the fragment
>
>   inverse : (a : C) -> Inverse {M = Mg} e a
>   inverse a  with  invMb a | inversionIsTotal a _
>   ...      | just (yes inv) | _  = inv
>   ...      | just (no _)    | ()
>   ...      | nothing        | ()
>
> It is type-checked in  Agda-2.3.2 MAlonzo,
>
> while changing the last line to      ...  | _ | ()
> leads to the report
>
> " Checking AlgClasses1 
> (/home/mechvel/doconA/0.01/source/AlgClasses1.agda).
>   Finished AlgClasses1.
>
> Failed to solve the following constraints:
>   [0] Is empty: justYes? .w \equiv┴║ Data.Bool.true
> "
>
> (without printing the line number).
>
> This looks strange, because the pattern set
>                             {just (yes inv), just (no _), nothing}
>
> is exhaustive for the type of  Maybe $ Dec $ Inverse {M = Mg} e a
> of  invMb a,
> hence the last wildcard needs to be replaced with `nothing'.
>
> Am I missing something?
>
> Regards,
>
> ------
> Sergei
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-- 
Andreas Abel  <><     Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich 
http://www.tcs.informatik.uni-muenchen.de/~abel/