hi MetaCoq devs, just to flag up I think this is a question you might be able answer (and also use to advertise MetaCoq to the proof assistant community): https://proofassistants.stackexchange.com/questions/1428/formal-description-of-coq-s-termination-checker

Thank you Karl, indeed we even have a preliminary implementation of a guard checker in Coq! I answered the question :)

Last updated: Feb 09 2023 at 02:02 UTC