<div dir="ltr"><div>Hi Joey,</div><div><br></div><div>I haven't tried it in this example, but in general it can help the termination checker to introduce more (mutual) helper functions to reduce the nesting of pattern matches so that the end result does only shallow pattern matching. So here you could have foldsO only pattern match on the first argument and delegate each of the cases to a helper function. I hope that helps.</div><div><br></div><div>-- Jesper<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, Apr 29, 2020 at 11:53 PM Joey Eremondi <<a href="mailto:joey.eremondi@gmail.com">joey.eremondi@gmail.com</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"><div dir="ltr"><div>Basically, I'm wondering if there's any way to make the following file pass the termination checker using the --without-K</div><div><br></div><div><a href="https://github.com/JoeyEremondi/spire.github.io/blob/debe0a3ebbb4c82388f4f5b785b955fbc02b3d4f/source/_code/2014-08-04-inductive-recursive-descriptions/IDescIR.agda" target="_blank">https://github.com/JoeyEremondi/spire.github.io/blob/debe0a3ebbb4c82388f4f5b785b955fbc02b3d4f/source/_code/2014-08-04-inductive-recursive-descriptions/IDescIR.agda</a></div><div><br></div><div>It's a nifty combination of Descriptions and Induction-Recursion thanks to Larry Diehl. However, if I add the --without-K flag, it complains about foldO and foldsO not terminating.</div><div><br></div><div>I'm assuming this is because of the issues described here: <a href="https://agda.readthedocs.io/en/v2.6.1/language/without-k.html#restrictions-on-termination-checking" target="_blank">https://agda.readthedocs.io/en/v2.6.1/language/without-k.html#restrictions-on-termination-checking</a></div><div><br></div><div>So I (roughly) understand the problem, but I have no idea if there's a solution. Is this simply not a well-founded definition when K is disabled? Or is there some trick I can use to massage this into something the termination checker will like?<br></div></div>
_______________________________________________<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>