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 (11)

Authors

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

Maintainers

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

Sources

2.1.0+8.17.tar.gz
md5=3b6a903bec36a3ea30b3a9ca32a71813
sha512=3d50ded6597b19c73a2fb7a4908ef33d7b38894879a655e158adbf3818e6dab657bffd11929c0f9a9b4f9fac87ef89995ff14fe51f3b72337a9847681d3c6c94

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

Module Waterproof.Wp_rewriteSource

Sourceval wp_autorewrite : ?print_hints:bool -> Backtracking.trace Proofview.tactic -> unit Proofview.tactic

Waterproof autorewrite

This tactic is a rewrite of the coq-core's autorewrite tactic that will only consider current hypothesis as rewrite hints.