package coq-waterproof

You can search for identifiers within the package.

in-package search v0.2.0

Coq proofs in a style that resembles non-mechanized mathematical proofs

Install

md5=3b6a903bec36a3ea30b3a9ca32a71813

sha512=3d50ded6597b19c73a2fb7a4908ef33d7b38894879a655e158adbf3818e6dab657bffd11929c0f9a9b4f9fac87ef89995ff14fe51f3b72337a9847681d3c6c94

Sourceval loaded_hint_dataset : string list ref

Contains the hint dataset that is currently loaded

val existing_datasets : 
  Hint_dataset_declarations.hint_dataset Proofutils.StringMap.t ref

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

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

Sets the databases of a given database_type in a given dataset

val 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