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. P
    Pim Otte
  3. B
    Balthazar Pathiachvili
  4. C
    Cosmin Manea
  5. L
    Lulof Pirée
  6. A
    Adrian Vrămuleţ
  7. T
    Tudor Voicu
  8. J
    Jim Portegies <j.w.portegies@tue.nl>

Maintainers

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

Sources

3.0.0+8.18.tar.gz
md5=32d187d47ea005e068a8b57dd4358cd3
sha512=67733e1ccc66b5e66dde0e52b33ece12ea253db0af4a0e690129f965f064546a5e415b2e5d8a3cac1df298178788273f334a2ddd83044c7ff7b88f7abbc9473f

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

Module Waterproof.Wp_bulletsSource

This module registers two new bullet behaviors available for use in Waterproof. With

Set Bullet Behavior "Waterproof Strict Subproofs".

one basically gets the default bullet behavior, with slightly different suggestion and error messages.

With

Set Bullet Behavior "Waterproof Relaxed Subproofs".

it doesn't matter which exact bullets one uses in a particular place: they all function the same.