package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (6)

Authors

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

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.3.0.tar.gz
sha256=3f0fc283e8644394aa9c7a6e3995b6d9ebbe1e6dda712bf431f9c372dcef95ad

doc/rocq-runtime.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.

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)

Sourceval check_fix_with_elims : Environ.env -> Evd.evar_map -> Constr.fixpoint -> Evd.evar_map

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

Sourcetype ('constr, 'types, 'r) bad_relevance =
  1. | BadRelevanceBinder of 'r * ('constr, 'types, 'r) Context.Rel.Declaration.pt
  2. | BadRelevanceCase of 'r * 'constr

Template typing

Sourceval get_template_parameters : Environ.env -> Evd.evar_map -> Names.inductive -> ?refresh_all:bool -> EConstr.unsafe_judgment array -> Evd.evar_map * Inductive.param_univs