package coq

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

Module TypeopsSource

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.

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

Type of sorts.

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

Type of a bound variable.

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

Type of variables

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

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

Sourceval type_of_int : Environ.env -> Constr.types
Sourceval type_of_float : Environ.env -> Constr.types
Sourceval warn_bad_relevance_name : string

Allow the checker to make this warning into an error.

Sourceval 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