Li-yao (Oct 24 2021 at 14:37): Li-yao (Oct 24 2021 at 14:37):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: Oct 13 2024 at 01:02 UTC