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 (3)

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.1.0.tar.gz
sha256=b236dc44f92e1eeca6877c7ee188a90c2303497fe7beb99df711ed5a7ce0d824

doc/rocq-runtime.proofs/Tacmach/index.html

Module TacmachSource

Operations for handling terms under a local typing context.

Variants of Tacmach functions built with the new proof engine

Sourceval pf_apply : (Environ.env -> Evd.evar_map -> 'a) -> Proofview.Goal.t -> 'a

This function does no type inference and expects an already well-typed term. It recomputes its type in the fastest way possible (no conversion is ever involved)

This function entirely type-checks the term and computes its type and the implied universe constraints.

Sourceval pf_conv_x : Proofview.Goal.t -> EConstr.t -> EConstr.t -> bool
Sourceval pf_get_new_id : Names.Id.t -> Proofview.Goal.t -> Names.Id.t
Sourceval pf_ids_of_hyps : Proofview.Goal.t -> Names.Id.t list
Sourceval pf_ids_set_of_hyps : Proofview.Goal.t -> Names.Id.Set.t
Sourceval pf_hyps_types : Proofview.Goal.t -> (Names.Id.t * EConstr.types) list