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/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