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-project

Dependency

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

Authors

T

The Rocq development team, INRIA, CNRS, and contributors

Maintainers

T

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

Sources

rocq-9.0.1.tar.gz

sha256=051f7bf702ff0a3b370449728921e5a95e18bc2b31b8eb949d48422888c98af4

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

Module `Evd.Expand`Source

Only used as EConstr internals

Sourcetype handle

Sourceval empty_handle : handle

Sourceval liftn_handle : int -> handle -> handle

val kind : 
  evar_map ->
  handle ->
  econstr ->
  handle
  * (econstr,
      econstr,
      MiniEConstr.ESorts.t,
      MiniEConstr.EInstance.t,
      MiniEConstr.ERelevance.t)
      Constr.kind_of_term

Sourceval expand : evar_map -> handle -> econstr -> econstr

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