Skip to content

Coq's Guard Checker in Coq 8.19

Latest
Compare
Choose a tag to compare
@SwampertX SwampertX released this 20 Aug 15:53

This guard checker implemented in Coq works with MetaCoq 1.3.2 and Coq 8.19. It implements the guard checker in Coq's kernel in the master branch, as recent as at the time of release (last commit: d6550d). Currently, it achieves full agreement with Coq's guard checker on Coq's guard checker test suite, except for slow reduction on some examples, which it didn't terminate within the time allowed.

Full Changelog: https://github.com/inria-cambium/m1-tan/commits/v1.0.0