You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
This is more of a question than a real issue, but I wasn't sure how best to reach folks, so I'm putting it here. I've been using MetaCoq and TemplateMonad for developing a plugin (it's really usable and slick, great job!) and it would be great to reason about the result of running TemplateMonad programs (even axiomatically).
Is there currently a way to do this, or plans (even tentative) to implement something like it? For example, it would be nice to reason about the effect of tmMkDefinition on the global environment, or the behavior of tmLocate, etc.
Thanks,
John
The text was updated successfully, but these errors were encountered:
Hello,
This is more of a question than a real issue, but I wasn't sure how best to reach folks, so I'm putting it here. I've been using MetaCoq and TemplateMonad for developing a plugin (it's really usable and slick, great job!) and it would be great to reason about the result of running TemplateMonad programs (even axiomatically).
Is there currently a way to do this, or plans (even tentative) to implement something like it? For example, it would be nice to reason about the effect of
tmMkDefinition
on the global environment, or the behavior oftmLocate
, etc.Thanks,
John
The text was updated successfully, but these errors were encountered: