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.0.1.tar.gz
sha256=051f7bf702ff0a3b370449728921e5a95e18bc2b31b8eb949d48422888c98af4

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

Module EConstr.ExpandSource

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 handle
Sourceval make : Evd.econstr -> handle * t
Sourceval liftn_handle : int -> handle -> handle
Sourceval kind : Evd.evar_map -> handle -> t -> handle * kind
Sourceval 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
Sourceval iter_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> handle -> t -> unit) -> 'a -> handle -> kind -> unit