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.1.tar.gz
md5=83359b33c0c6e1fb87f938280cd4e0a2
sha512=d0b0d674e9b5c731b54779d9b77b61f6142d561b05e8c06f2afd0a62e507afedd7696754d29c31522fee996a1f6c6a5d158b250ab04fd9dd5bd812bb99d3a97f

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

Module Waterproof.Unfold_frameworkSource

In this module we keep two tables:

  • wp_unfold_map a map from strings to global references, that is used to keep track of the introduced notations, and the global reference they are associated with
  • wp_unfold_tbl a table from global references to unfold actions, that can later be used by the unfold framework. The unfold actions can be of three types:
  • unfold the definition associated to the global reference
  • apply a bi-implication
  • rewrite an equality
Sourcetype unfold_action =
  1. | Unfold of string * Names.GlobRef.t
  2. | Apply of string * EConstr.constr
  3. | Rewrite of string * EConstr.constr

A type to represent the different unfold actions, and the data they need.

Sourcetype unfold_entry =
  1. | Unfold_entry of string
  2. | Apply_entry of string * Constrexpr.constr_expr
  3. | Rewrite_entry of string * Constrexpr.constr_expr

A type that represents the datastructure that can be added to the unfold table. When it is added, it will be converted to an unfold action.

Sourcemodule StringMap : Map.S with type key = string
Sourceval wp_unfold_map : Names.GlobRef.t StringMap.t ref
Sourceval add_to_unfold_map : string list -> Names.GlobRef.t -> unit
Sourceval register_unfold : string list -> Libnames.qualid -> Ltac2_plugin.Tac2entries.notation_interpretation_data * Ltac2_plugin.Tac2entries.notation_interpretation_data
Sourceval register_unfold_entry : Names.GlobRef.t -> unfold_entry -> unit
Sourceval extract_def : string -> Names.GlobRef.t option
Sourceval wp_unfold_tbl : (Names.GlobRef.t, unfold_action) Hashtbl.t ref
Sourceval find_unfold_actions_by_ref : Names.GlobRef.t -> unfold_action list
Sourceval find_unfold_actions_by_str : string -> unfold_action list
Sourceval get_all_references : unit -> Names.GlobRef.t list