package coq-waterproof

You can search for identifiers within the package.

in-package search v0.2.0

Coq proofs in a style that resembles non-mechanized mathematical proofs

Install

Dune Dependency

github.com Readme Changelog Edit opam file Versions (6)

Authors

Maintainers

J

Jim Portegies <j.w.portegies@tue.nl>

Sources

2.2.0+8.20.tar.gz

md5=18c6dafc6fb018f167f89fb236ff494b

sha512=096ebe52912ebe3fb063a5ce88bee1dfc8f63226f7f1284a4304a079751b98c617a4fcafa9781c3e54e024e631c87248885b56efc20086c98ae0e525cfe08efb

doc/coq-waterproof.plugin/Waterproof/Wp_evars/index.html

Module `Waterproof.Wp_evars`Source

Sourceval is_blank : Evd.evar_map -> Evar.t -> bool

Checks whether a given evar is a blank (entered by the user with the `_` syntax) in the evar_map.

Sourceval refine_goal_with_evar : string -> unit Proofview.tactic

Refines the current goal with just a new named evar, the name of which is based on the input string. The use of this is to replace unnamed evars with named ones, so that the user can refer to them later.

Sourceval blank_evars_in_term : Evd.econstr -> Evar.t list Proofview.tactic

A tactic that resturns a list of all evars in a term (= Evd.econstr) that were introduced by the user as a blank and have not been resolved yet.