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