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/Exceptions/index.html

Module Waterproof.ExceptionsSource

Sourceval filter_errors : bool ref

A flag that determines whether Waterproof should filter errors

Sourceval feedback_log : Feedback.level -> Pp.t list ref

A rudimentary feedback log

Sourceval wp_feedback_logger_id : int option ref

The id that we obtained when registering wp_feedback_logger as a feeder in Feedback.mli

Sourceval wp_feedback_logger : Feedback.feedback -> unit

Our own logger that we add as a feeder to Coq's feedback mechanism in Feedback.mli

Sourceval add_wp_feedback_logger : unit -> unit

Adds the wp_feedback_logger to Coq's feeedback mechanism

Sourceval print_hypothesis_help : bool ref

Should hypothesis hints be printed (For instance on how you can use a forall statement)?

Sourceval last_thrown_warning : Pp.t option ref

The last thrown warning

Sourceval redirect_feedback : bool ref

Redirect warnings: this is useful when testing the plugin: meant to redirect Waterproof errors directly to the log

Sourceval redirect_errors : bool ref

Redirect errors: this is useful when testing the plugin: meant to redirect errors to Control.zero rather than CErrors.user_err

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 notice : Pp.t -> unit Proofview.tactic

Sends a notice

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

Send an info message

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

Throws an error

Sourceval message : Feedback.level -> Pp.t -> unit Proofview.tactic

A general function for sending feedback

Sourceval get_last_warning : unit -> Pp.t option Proofview.tactic

Check the last warning against a string