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

Authors

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

Maintainers

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

Sources

2.0.1+8.17.tar.gz
md5=a891f29ee1723d8031d4cb50903da735
sha512=cfc7a8010b71ab45264f396b144f0cf887baf9ddae9df1e92d977252801197017225af0d4bbabaf7a0b57454aa2ce68989c58ce6c1707b4bc40674488bf0a622

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