Karl Palmskog (May 25 2022 at 12:00): Karl Palmskog (May 25 2022 at 12:00):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
Yannick Forster (May 25 2022 at 12:15):Thank you Karl, indeed we even have a preliminary implementation of a guard checker in Coq! I answered the question :)
Last updated: Jun 01 2023 at 11:01 UTC