package coq-waterproof
Coq proofs in a style that resembles non-mechanized mathematical proofs
Install
Dune Dependency
Authors
Maintainers
Sources
2.2.0+8.17.tar.gz
md5=cd4867e94e20eba727bd6deea06130cd
sha512=1205227101bb30f3e8c4ec05217920dcda1e3631ecd0428f2ac820c9a2811f91526d68623aaf01dd9aa1e81e8adfc083af01152d7f7a6e48894caa829bc3f440
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.