package coq-waterproof
Coq proofs in a style that resembles non-mechanized mathematical proofs
Install
Dune Dependency
Authors
Maintainers
Sources
2.1.1+8.18.tar.gz
md5=a7d2922fb4ed7f0b8fe38074319890fe
sha512=3c511d066ba324cf19fc5620ae89ad09796f3a04576012739783100487dd8d50214edab9bdfc85d581d6538e601511f4563b90ad1dc3041e60a9702f4875e31d
doc/coq-waterproof.plugin/Waterproof/Wp_eauto/index.html
Module Waterproof.Wp_eautoSource
Source
val esearch :
bool ->
int ->
Tactypes.delayed_open_constr list ->
Hints.hint_db list ->
Pp.t list ->
Pp.t list ->
Backtracking.trace Proofview.tacticSearches a sequence of at most n tactics within db_list and lems that solves the goal
The goal can contain evars
Source
val wp_eauto :
bool ->
int ->
Tactypes.delayed_open_constr list ->
string list ->
Backtracking.trace Proofview.tacticWaterproof eauto
This function is a rewrite around Eauto.eauto with the same arguments to be able to retrieve which hints have been used in case of success.
The code structure has been rearranged to match the one of wp_auto.wp_auto.
Source
val rwp_eauto :
bool ->
int ->
Tactypes.delayed_open_constr list ->
Hints.hint_db_name list ->
Pp.t list ->
Pp.t list ->
Backtracking.trace Proofview.tacticRestricted Waterproof eauto
This function acts the same as wp_auto but will fail if all proof found contain at least one must-use lemma that is unused or one hint that is in the forbidden list.