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