package rocq-runtime

  1. Overview
  2. Docs
package rocq-runtime
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

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