MetaCoq / metacoq

Metaprogramming, verified meta-theory and implementation of Coq in Coq
https://metacoq.github.io
MIT License
380 stars 82 forks source link

Add MCListable class for enumerating finite types #962

Closed JasonGross closed 1 year ago

JasonGross commented 1 year ago

This will be useful for proving that quotation of byte is well-typed with the safechecker.