Add the `force (lazy t)` evaluation rule to LambdaBox

MetaCoq / metacoq

Metaprogramming, verified meta-theory and implementation of Coq in Coq

https://metacoq.github.io

MIT License

367 stars 79 forks source link

Add the `force (lazy t)` evaluation rule to LambdaBox #1089

Closed mattam82 closed 2 months ago

mattam82 commented 2 months ago

All the evaluation relations have been updated. Note that this is not in the target of erasure, it is only used by the yet unverified cofix->fix translation.