package coq

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

Module Safe_typingSource

Sourcetype vodigest =
  1. | Dvo_or_vi of Digest.t
  2. | Dvivo of Digest.t * Digest.t
Sourceval digest_match : actual:vodigest -> required:vodigest -> bool
Safe environments

Since we are now able to type terms, we can define an abstract type of safe environments, where objects are typed before being added.

We also provide functionality for modules : start_module, end_module, etc.

Sourcetype safe_environment
Sourcetype section_data
Sourceval empty_environment : safe_environment
Sourceval is_initial : safe_environment -> bool
Sourceval env_of_safe_env : safe_environment -> Environ.env
Sourceval sections_of_safe_env : safe_environment -> section_data Section.t option
Sourceval structure_body_of_safe_env : safe_environment -> Declarations.structure_body

The safe_environment state monad

Sourcetype safe_transformer0 = safe_environment -> safe_environment
Sourcetype 'a safe_transformer = safe_environment -> 'a * safe_environment
Stm machinery
Sourcetype private_constants
Sourceval empty_private_constants : private_constants
Sourceval is_empty_private_constants : private_constants -> bool

concat_private e1 e2 adds the constants of e1 to e2, i.e. constants in e1 must be more recent than those of e2.

Sourceval push_private_constants : Environ.env -> private_constants -> Environ.env

Push the constants in the environment if not already there.

Sourceval universes_of_private : private_constants -> Univ.ContextSet.t
Sourceval is_curmod_library : safe_environment -> bool
Sourceval join_safe_environment : ?except:Future.UUIDSet.t -> safe_environment -> safe_environment
Sourceval is_joined_environment : safe_environment -> bool

Enriching a safe environment

Insertion of global axioms or definitions

Sourcetype exported_private_constant = Names.Constant.t

returns the main constant

Similar to add_constant but also returns a certificate

Adding an inductive type

Adding a module or a module type

Adding universe constraints

Sourceval push_context_set : strict:bool -> Univ.ContextSet.t -> safe_transformer0

Setting the type theory flavor

Sourceval set_indices_matter : bool -> safe_transformer0
Sourceval set_share_reduction : bool -> safe_transformer0
Sourceval set_check_guarded : bool -> safe_transformer0
Sourceval set_check_positive : bool -> safe_transformer0
Sourceval set_check_universes : bool -> safe_transformer0
Sourceval set_VM : bool -> safe_transformer0
Sourceval set_native_compiler : bool -> safe_transformer0
Sourceval set_allow_sprop : bool -> safe_transformer0
Sourceval check_engagement : Environ.env -> Declarations.set_predicativity -> unit
Interactive section functions
Sourceval open_section : safe_transformer0
Sourceval close_section : safe_transformer0
Sourceval sections_are_opened : safe_environment -> bool

Insertion of local declarations (Local or Variables)

Sourceval push_named_assum : (Names.Id.t * Constr.types) -> safe_transformer0
Sourceval push_section_context : (Names.Name.t array * Univ.UContext.t) -> safe_transformer0

Add local universes to a polymorphic section

Interactive module functions
Sourceval allow_delayed_constants : bool ref

Traditional mode: check at end of module that no future was created.

The optional result type is given without its functorial part

Sourceval current_modpath : safe_environment -> Names.ModPath.t
Sourceval current_dirpath : safe_environment -> Names.DirPath.t
Libraries : loading and saving compilation units
Sourcetype compiled_library
Sourceval univs_of_library : compiled_library -> Univ.ContextSet.t
Safe typing judgments
Sourcetype judgment

The safe typing of a term returns a typing judgment.

Queries
Sourceval exists_objlabel : Names.Label.t -> safe_environment -> bool
Sourceval constant_of_delta_kn_senv : safe_environment -> Names.KerName.t -> Names.Constant.t
Sourceval mind_of_delta_kn_senv : safe_environment -> Names.KerName.t -> Names.MutInd.t
Retroknowledge / Native compiler
Sourceval register_inline : Names.Constant.t -> safe_transformer0
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