package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.17.1.tar.gz
sha512=9a35311acec2a806730b94ac7dceabc88837f235c52a14c026827d9b89433bd7fa9555a9fc6829aa49edfedb24c8bbaf1411ebf463b74a50aeb17cba47745b6b
doc/coq-core.engine/Proofview/Goal/index.html
Module Proofview.Goal
Source
Type of goals.
concl
, hyps
, env
and sigma
given a goal gl
return respectively the conclusion of gl
, the hypotheses of gl
, the environment of gl
(i.e. the global environment and the hypotheses) and the current evar map.
enter t
applies the goal-dependent tactic t
in each goal independently, in the manner of tclINDEPENDENT
except that the current goal is also given as an argument to t
.
Like enter
, but assumes exactly one goal under focus, raising a fatal error otherwise.
Recover the list of current goals under focus, without evar-normalization. FIXME: encapsulate the level in an existential type.
unsolved g
is true
if g
is still unsolved in the current proof state.
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>