package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (3)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.0.1.tar.gz
sha256=051f7bf702ff0a3b370449728921e5a95e18bc2b31b8eb949d48422888c98af4

doc/rocq-runtime.vernac/Declare/Hook/index.html

Module Declare.HookSource

Declaration hooks, to be run when a constant is saved. Use with care, as imperative effects may become not supported in the future.

Sourcetype 'a g
Sourcetype t = unit g
Sourcemodule S : sig ... end

Hooks allow users of the API to perform arbitrary actions at proof/definition saving time. For example, to register a constant as a Coercion, perform some cleanup, update the search database, etc...

Sourceval make_g : (S.t -> 'a -> 'a) -> 'a g
Sourceval make : (S.t -> unit) -> t
Sourceval call : ?hook:t -> S.t -> unit