<div dir="ltr"><div>Here is one easy counterexample for the first question:<br></div><div><br></div><div>plus : Nat → Nat → Nat<br>plus x y = {!!}</div><div><br></div><div>-- split on y:</div><div><br></div><div>plus : Nat → Nat → Nat<br>plus x zero = {!!}<br>plus x (suc y) = {!!}</div><div><br></div><div>-- with point still in first hole, split on x:</div><div><br></div><div>plus : Nat → Nat → Nat<br>plus zero zero = {!!}<br>plus (suc x) zero = {!!}<br>plus x (suc y) = {!!}</div><div><br></div><div>Now we've got an --exact-split warning for the last line.<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, Feb 12, 2021 at 1:35 PM Martin Escardo <<a href="mailto:m.escardo@cs.bham.ac.uk">m.escardo@cs.bham.ac.uk</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><br>
I have a development that uses --exact-split in all modules.<br>
<br>
But I have a function I can't make to satisfy --exact-split.<br>
<br>
I developed this function using case-split.<br>
<br>
One question is: shouldn't be the case that if all pattern matching is<br>
developed not manually but mechanically using case-split, then<br>
--exact-split should be automatically satisfied?<br>
<br>
At first I thought this could have something to do with the simultaneous<br>
use of --without-K. But then I removed all pattern matching on<br>
identifications, using helper functions that pass the --exact-split test.<br>
<br>
The main question is: what promises does --exact-split (not) make, and<br>
what promises should I, as its user, fulfill?<br>
<br>
Martin<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>