package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type
type 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).

type oracle
val empty : oracle
val 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.

type 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.

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

Check whether a level is transparent

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

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

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

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

val 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