package coq
Formal proof management system
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.14.0.tar.gz
sha256=b1501d686c21836302191ae30f610cca57fb309214c126518ca009363ad2cd3c
doc/coq-core.kernel/Conv_oracle/index.html
Module Conv_oracle
Source
Source
val oracle_order :
('a -> Names.Constant.t) ->
oracle ->
bool ->
'a Names.tableKey ->
'a Names.tableKey ->
bool
Order on section paths for unfolding. If oracle_order kn1 kn2
is true, then unfold kn1 first. Note: the oracle does not introduce incompleteness, it only tries to postpone unfolding of "opaque" constants.
Priority for the expansion of constant in the conversion test. * Higher levels means that the expansion is less prioritary. * (And Expand stands for -oo, and Opaque +oo.) * The default value (transparent constants) is Level 0
.
Sets the level of a constant. * Level of RelKey constant cannot be set.
Source
val fold_strategy :
(Names.Constant.t Names.tableKey -> level -> 'a -> 'a) ->
oracle ->
'a ->
'a
Fold over the non-transparent levels of the oracle. Order unspecified.
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>