[Agda] How to engage coverage checking

[Ulf Norell]

On Sat, Nov 22, 2008 at 5:02 PM, Jim Apple
<jbapple+agda at gmail.com<jbapple%2Bagda at gmail.com>
> wrote:

> The following compiles (and loads into the interactive mode) fine with
> v2.1.2:
>
> module Cover where
>
> data Nat : Set where
>     Z : Nat
>     S : Nat -> Nat
>
> sum : Nat -> Nat -> Nat
> sum Z m = m
>
> How do I ask Agda to check if sum is total?


v2.1.2 doesn't have a coverage checker. Later versions do.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20081122/a48928ac/attachment.html