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

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.20.tar.gz
md5=2e3f1ff03321f487b6fbe4a3cfbd3fd5
sha512=a250247ad200b05ee355096526c68eb0ce19622e5c1e9eb15db4f3a522de1ae946cae2b14644d4e124ca13954e89f655dab8d73c7d4f1e8b8206989e2acd64fd

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