package coq-waterproof

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Change log for the coq-waterproof library

Converted coq library to coq plugin
Automation procedures are now handled internally in the plugin, so that they can be customized and so that one can check the use of certain lemmas within the automation

Added and updated theory files.
Reorganized automation libraries.
Added goal wrappers that force user to write sentences that make proofscript more readable.
Support chains of (in)equalities for =, < and <= in naturals and reals.
Fixed issues with several tactics, including Take ....
Rephrased multiple tactics like Obtain ... according to ..., ....
For propositions, have user specify types rather than labels in tactics. Labeling is now optional.
Added some shielding for use of automation, e.g. statements starting with quantifiers cannot be proved automatically.