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.0.tar.gz
md5=7cfe30aceb61e154ed905e048bdf2cb7
sha512=006bf05727d2aa21cebe332ff5a027fdd8843c574753fd5b8d0486e4df7bd447a4f538c3c92736011734c29c601d3a77c2f1a1ee5b3645a7666766ed32907777

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