search

MetaCoq / metacoq

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

Guard condition not depending on contexts #504

Closed fakusb closed 3 years ago

fakusb commented 4 years ago

The current abstraction for the guard condition does not allow the guard condition to depend on the local or global environment, as it only takes a term as an argument.

The guard condition implemented in Coq does unfold definitions while checking guardedness, so it could not instantiate this abstraction. For faithfulness, this might be an issue.

mattam82 commented 3 years ago

I will update it with the global and local contexts.

mattam82 commented 3 years ago

This has been handled in PR #524