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 (3)

Authors

  1. J
    Jelle Wemmenhove
  2. P
    Pim Otte
  3. B
    Balthazar Pathiachvili
  4. D
    Dick Arends
  5. C
    Cosmin Manea
  6. L
    Lulof Pirée
  7. A
    Adrian Vrămuleţ
  8. T
    Tudor Voicu
  9. J
    Jim Portegies <j.w.portegies@tue.nl>

Maintainers

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

Sources

3.1.0+9.0.tar.gz
md5=7cfe30aceb61e154ed905e048bdf2cb7
sha512=006bf05727d2aa21cebe332ff5a027fdd8843c574753fd5b8d0486e4df7bd447a4f538c3c92736011734c29c601d3a77c2f1a1ee5b3645a7666766ed32907777

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

Module Waterproof.Hint_datasetSource

Sourceval loaded_hint_dataset : string list ref

Contains the hint dataset that is currently loaded

Dictionary with dataset names as keys and datasets as values

Sourceval load_dataset : string -> unit

Replace all current loaded hints by the ones declared in the hint_dataset

Sourceval remove_dataset : string -> unit

Removes a dataset to the currently loaded hint datasets

Sourceval clear_dataset : unit -> unit

Clears all the currently loaded datasets

Sourceval create_new_dataset : string -> unit

Creates a new empty dataset from a given name

Sourceval populate_dataset : string -> Hint_dataset_declarations.database_type -> string list -> unit

Sets the databases of a given database_type in a given dataset

Sourceval get_current_databases : Hint_dataset_declarations.database_type -> Hints.hint_db_name list

Returns the list of databases of the current loaded dataset for the given Hint_dataset_declarations.database_type