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.1+8.17.tar.gz
md5=246900c584d34deb5a4ed74e74c3aeab
sha512=f5242890a140c6966bd76e1d487a8ca139c14874eb0c1a589f28b72773be24f11f07bb1b163153c5811330a28a91a94d508233dc19849baa671fada857f05a3b

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

Module Waterproof.ExceptionsSource

Sourcetype wexn =
  1. | CastError of string
    (*

    Indicates that a cast made by the FFI has failed

    *)
  2. | FailedAutomation of string
    (*

    Indicates that the automatic solver called has failed

    *)
  3. | FailedTest of string
    (*

    Indicates that the running test has failed

    *)
  4. | NonExistingDataset of Hints.hint_db_name
    (*

    Indicates that the user tried to import a non-existing hint dataset

    *)
  5. | UnusedLemmas
    (*

    Indicates that no proof using all the given lemmas has been found

    *)
  6. | ToUserError of Pp.t
    (*

    An error that should go directly to the user

    *)

Type of exceptions used in Wateproof

Sourceval throw : ?info:Exninfo.info -> wexn -> 'a

Throws an error with given info and message

Sourceval warn : Pp.t -> unit Proofview.tactic

Sends a warning

Sourceval err : Pp.t -> unit Proofview.tactic

Throws an error