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

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.2.0.tar.gz
sha256=a45280ab4fbaac7540b136a6b073b4a6db15739ec1e149bded43fa6f4fc25f20

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