package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Conv_oracleSource

Sourcetype evaluable =
  1. | EvalVarRef of Names.Id.t
  2. | EvalConstRef of Names.Constant.t
  3. | EvalProjectionRef of Names.Projection.Repr.t

Evaluable references (whose transparency can be controlled).

Sourcetype oracle
Sourceval empty : oracle
Sourceval oracle_order : oracle -> bool -> evaluable option -> evaluable option -> 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.

Sourcetype level =
  1. | Expand
  2. | Level of int
  3. | Opaque

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.

Sourceval pr_level : level -> Pp.t
Sourceval transparent : level
Sourceval is_transparent : level -> bool

Check whether a level is transparent

Sourceval get_strategy : oracle -> evaluable -> level
Sourceval set_strategy : oracle -> evaluable -> level -> oracle

Sets the level of a constant. * Level of RelKey constant cannot be set.

Sourceval fold_strategy : (evaluable -> level -> 'a -> 'a) -> oracle -> 'a -> 'a

Fold over the non-transparent levels of the oracle. Order unspecified.

Sourceval get_transp_state : oracle -> TransparentState.t
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct