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

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.2.0.tar.gz
sha256=a45280ab4fbaac7540b136a6b073b4a6db15739ec1e149bded43fa6f4fc25f20

doc/rocq-runtime.tactics/Redexpr/User/index.html

Module Redexpr.UserSource

Sourcetype ('raw, 'glb) user_red_spec = {
  1. ured_intern : Constrintern.ltac_sign -> 'raw -> 'glb;
  2. ured_subst : Mod_subst.substitution -> 'glb -> 'glb;
  3. ured_eval : 'glb -> Reductionops.e_reduction_function * Constr.cast_kind;
  4. ured_rprint : Environ.env -> Evd.evar_map -> 'raw -> Pp.t;
  5. ured_gprint : Environ.env -> Evd.evar_map -> 'glb -> Pp.t;
}
Sourcetype ('raw, 'glb) user_red

User-defined reductions are indexed by the kind of payload they contain at both raw and glob levels.

Sourceval create : string -> ('raw, 'glb) user_red_spec -> ('raw, 'glb) user_red

Create a new user-defined reduction.

Sourceval make : ('raw, 'glb) user_red -> 'raw -> Genarg.rlevel user_red_expr

Inject the required data into a user reduction expression.