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: Jun 23 2024 at 23:01 UTC