Fetching latest commit…
Cannot retrieve the latest commit at this time.
|Failed to load latest commit information.|
An example of Coq plugin that provides a tactic that generalize the vm_compute tactic, such that it is possible to use it when existential variables appear in the goal. It also makes it possible to recover some kind of opacity by abstracting over some definitions that appear in the goal (instances of these definitions that appear through computations are going to be expanded, though). For instance, \[ evm blacklist [plus] \] in the goal \[ 5 * 4 + ?3 \] reduces to \[ 20 + ?3 \] INSTALL ================= make make install USAGE ================= - [evm_compute] perform computation using the vm_compute strategy, even if there are evars in the goal. - [evm_compute blacklist l] performs computation without unfolding the terms in [l] that appears in the current conclusion (but those that appear through reduction are unfolded). [l] is a list in OCaml syntax (bracketed, semi-colon separated).