package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
Typing functions (not yet tagged as safe)

They return unsafe judgments that are "in context" of a set of (local) universe variables (the ones that appear in the term) and associated constraints. In case of polymorphic definitions, these variables and constraints will be generalized.

When typechecking a term it may be updated to fix relevance marks. Do not discard the result.

Basic operations of the typing machine.

If j is the judgement $ c:t $ , then assumption_of_judgement env j returns the type $ c $ , checking that $ t $ is a sort.

val assumption_of_judgment : Environ.env -> Environ.unsafe_judgment -> Sorts.relevance
val type1 : Constr.types

Type of sorts.

val type_of_sort : Sorts.t -> Constr.types
val judge_of_prop : Environ.unsafe_judgment
val judge_of_set : Environ.unsafe_judgment
val type_of_relative : Environ.env -> int -> Constr.types

Type of a bound variable.

val judge_of_relative : Environ.env -> int -> Environ.unsafe_judgment
val type_of_variable : Environ.env -> Names.variable -> Constr.types

Type of variables

val judge_of_variable : Environ.env -> Names.variable -> Environ.unsafe_judgment
val type_of_constant_in : Environ.env -> Constr.pconstant -> Constr.types

type of a constant

type of an applied projection

Type of application.

Type of an abstraction.
val sort_of_product : Environ.env -> Sorts.t -> Sorts.t -> Sorts.t

Type of a product.

s Type of a let in.

Type of a cast.

Inductive types.

Type of global references.
val type_of_global_in_context : Environ.env -> Names.GlobRef.t -> Constr.types * Univ.AbstractContext.t

Returns the type of the global reference, by creating a fresh instance of polymorphic references and computing their instantiated universe context. The type should not be used without pushing it's universe context in the environmnent of usage. For non-universe-polymorphic constants, it does not matter.

Miscellaneous.
val check_hyps_inclusion : Environ.env -> ?evars:(Constr.existential -> Constr.constr option) -> Names.GlobRef.t -> Constr.named_context -> unit

Check that hyps are included in env and fails with error otherwise

Types for primitives

val type_of_int : Environ.env -> Constr.types
val type_of_float : Environ.env -> Constr.types
val judge_of_float : Environ.env -> Float64.t -> Environ.unsafe_judgment
val type_of_array : Environ.env -> Univ.Instance.t -> Constr.types
val warn_bad_relevance_name : string

Allow the checker to make this warning into an error.

val should_invert_case : Environ.env -> Constr.case_info -> bool

We have case inversion exactly when going from irrelevant nonempty (ie 1 constructor) inductive to relevant type.

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