Stream: Coq users

Topic: Termination checking rules


view this post on Zulip 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: Feb 05 2023 at 22:03 UTC