package rocq-runtime

You can search for identifiers within the package.

in-package search v0.2.0

The Rocq Prover -- Core Binaries and Tools

Install

Dune Dependency

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

Authors

T

The Rocq development team, INRIA, CNRS, and contributors

Maintainers

T

The Rocq development team <coqdev@inria.fr>

Sources

rocq-9.0.0.tar.gz

md5=8d522602d23e7a665631826dab9aa92b

sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be

doc/rocq-runtime.engine/EConstr/Expand/index.html

Module `EConstr.Expand`Source

Sourcetype t

A variant of EConstr.t where evar substitution is performed on the fly. The handle type below is a kind of substitution that is needed to make sense of the delayed term. Such representation is more efficient than EConstr.t when iterating over a whole term.

Caveat: the kind function below only returns the expanded head of the term. This means that when it returns Evar (evk, inst), evk is guaranteed to be undefined in the evar map but inst is, in general, not the same as you would get after expansion. You must call expand_instance before performing any operation on it.

Sourcetype kind = (t, t, ESorts.t, EInstance.t, ERelevance.t) Constr.kind_of_term

Sourcetype handle

Sourceval make : Evd.econstr -> handle * t

Sourceval repr : Evd.evar_map -> handle -> t -> Evd.econstr

Sourceval liftn_handle : int -> handle -> handle

Sourceval kind : Evd.evar_map -> handle -> t -> handle * kind

Source

val expand_instance : 
  skip:bool ->
  Evd.undefined Evd.evar_info ->
  handle ->
  t SList.t ->
  t SList.t

Sourceval iter : Evd.evar_map -> (handle -> t -> unit) -> handle -> kind -> unit