[Agda] --exact-split

[Tom Jack]

Here is one easy counterexample for the first question:

plus : Nat → Nat → Nat
plus x y = {!!}

-- split on y:

plus : Nat → Nat → Nat
plus x zero = {!!}
plus x (suc y) = {!!}

-- with point still in first hole, split on x:

plus : Nat → Nat → Nat
plus zero zero = {!!}
plus (suc x) zero = {!!}
plus x (suc y) = {!!}

Now we've got an --exact-split warning for the last line.

On Fri, Feb 12, 2021 at 1:35 PM Martin Escardo <m.escardo at cs.bham.ac.uk>
wrote:

>
> I have a development that uses --exact-split in all modules.
>
> But I have a function I can't make to satisfy --exact-split.
>
> I developed this function using case-split.
>
> One question is: shouldn't be the case that if all pattern matching is
> developed not manually but mechanically using case-split, then
> --exact-split should be automatically satisfied?
>
> At first I thought this could have something to do with the simultaneous
> use of --without-K. But then I removed all pattern matching on
> identifications, using helper functions that pass the --exact-split test.
>
> The main question is: what promises does --exact-split (not) make, and
> what promises should I, as its user, fulfill?
>
> Martin
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20210212/f19f0b9f/attachment.html>