package coq-waterproof

  1. Overview
  2. Docs
Coq proofs in a style that resembles non-mechanized mathematical proofs

Install 

dune-project
 Dependency

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

Authors

  1. J
    Jelle Wemmenhove
  2. P
    Pim Otte
  3. B
    Balthazar Pathiachvili
  4. D
    Dick Arends
  5. C
    Cosmin Manea
  6. L
    Lulof Pirée
  7. A
    Adrian Vrămuleţ
  8. T
    Tudor Voicu
  9. J
    Jim Portegies <j.w.portegies@tue.nl>

Maintainers

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

Sources

3.1.0+9.1.tar.gz
md5=83359b33c0c6e1fb87f938280cd4e0a2
sha512=d0b0d674e9b5c731b54779d9b77b61f6142d561b05e8c06f2afd0a62e507afedd7696754d29c31522fee996a1f6c6a5d158b250ab04fd9dd5bd812bb99d3a97f

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

Module Waterproof.Wp_evarsSource

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.