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.17.tar.gz
md5=0d402d92c1d3309dcb01fcbdb7f72c37
sha512=7a82041ef05b3edd0fbe2f63507a7ce7d910f6bf3f2a5d615b0c6f55986fd60ae2d5006983929d08a63a3a2c917801709aa4a47d2c1161a2d72d223081d341a9

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