• Jakob Botsch Nielsen's avatar
    Add contract_induction tactic · 6b7b7d05
    Jakob Botsch Nielsen authored
    This tactic applies contract_centric with evars and puts the "establish
    facts" obligation last. This allows the user to instantiate these during
    the proof of the property.
    6b7b7d05
Name
Last commit
Last update
theories Loading commit data...
vendor/record-update Loading commit data...
.editorconfig Loading commit data...
.gitignore Loading commit data...
.gitlab-ci.yml Loading commit data...
Makefile Loading commit data...
README.md Loading commit data...
_CoqProject Loading commit data...