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

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.3.0.tar.gz
sha256=3f0fc283e8644394aa9c7a6e3995b6d9ebbe1e6dda712bf431f9c372dcef95ad

doc/rocq-runtime.pretyping/GenConstr/index.html

Module GenConstrSource

Sourcetype ('raw, 'glb) tag

Tags for extensible terms. The raw type is contained in constrexpr, and the glb type in glob terms.

Sourceval create : string -> (_, _) tag

Create a new tag. Tags should be registered with GlobEnv.register_constr_interp0, Genintern.register_intern_constr, Gensubst.register_constr_subst and Genprint.register_constr_print.

Also optionally

  • Genintern.register_ntn_subst0 (to be used in notations)
  • Genintern.register_intern_pat and Genintern.register_interp_pat (to be used in tactic patterns)
Sourceval eq : ('raw1, 'glb1) tag -> ('raw2, 'glb2) tag -> ('raw1 * 'glb1, 'raw2 * 'glb2) Util.eq option
Sourceval repr : (_, _) tag -> string
Sourcetype any_tag =
  1. | Any : (_, _) tag -> any_tag
Sourceval name : string -> any_tag option
Sourcetype raw =
  1. | Raw : ('raw, _) tag * 'raw -> raw
Sourcetype glb =
  1. | Glb : (_, 'glb) tag * 'glb -> glb
Sourcemodule Register (M : sig ... end) : sig ... end