Is there a place where Coq's current termination checking rules are fully spelled out? The paper that the reference manual cites (in Gimenez's "Codifying guarded definitions with recursion schemes") handles the simple cases where you only use `match`

, but I'm wondering exactly how complex the algorithm gets when you also allow nested `fix`

. Is it just an ugly control-flow analysis, or is there a neat trick to it?

Last updated: Feb 05 2023 at 22:03 UTC