package coq-core

  1. Overview
  2. Docs
The Coq Proof Assistant -- Core Binaries and Tools

Install 

dune-project
 Dependency

coq.inria.fr Readme Edit opam file Versions (11)

Authors

  1. T
    The Coq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Coq development team <coqdev@inria.fr>

Sources

coq-8.17.1.tar.gz
sha512=9a35311acec2a806730b94ac7dceabc88837f235c52a14c026827d9b89433bd7fa9555a9fc6829aa49edfedb24c8bbaf1411ebf463b74a50aeb17cba47745b6b

doc/coq-core.pretyping/Typing/index.html

Module TypingSource

This module provides the typing machine with existential variables and universes.

Sourceval type_of : ?refresh:bool -> Environ.env -> Evd.evar_map -> EConstr.constr -> Evd.evar_map * EConstr.types

Typecheck a term and return its type + updated evars, optionally refreshing universes

Typecheck a type and return its sort

Typecheck a term has a given type (assuming the type is OK)

Sourceval type_of_variable : Environ.env -> Names.variable -> EConstr.types

Type of a variable.

Returns the instantiated type of a metavariable

Solve existential variables using typing

Raise an error message if incorrect elimination for this inductive (first constr is term to match, second is return predicate)

Raise an error message if bodies have types not unifiable with the expected ones

Variant of check that assumes that the argument term is well-typed.

Sourceval judge_of_sprop : EConstr.unsafe_judgment
Sourceval judge_of_prop : EConstr.unsafe_judgment

hack