package coq
Formal proof management system
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.15.1.tar.gz
sha256=513e953b7183d478acb75fd6e80e4dc32ac1a918cf4343ac31a859cfb4e9aad2
doc/coq-core.vernac/Declare/Hook/index.html
Module Declare.Hook
Source
Declaration hooks, to be run when a constant is saved. Use with care, as imperative effects may become not supported in the future.
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...
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>