<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">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">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>