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/index.html

Module RedexprSource

Interpretation layer of redexprs such as hnf, cbv, etc.

Sourcetype 'l user_red_expr

User-defined reductions

Sourceval pr_raw_user_red_expr : Environ.env -> Evd.evar_map -> Genarg.rlevel user_red_expr -> Pp.t
Sourceval pr_glob_user_red_expr : Environ.env -> Evd.evar_map -> Genarg.glevel user_red_expr -> Pp.t
Sourcetype red_expr_val
Sourceval out_with_occurrences : 'a Locus.with_occurrences_expr -> 'a Locus.with_occurrences
Sourceval eval_red_expr : Environ.env -> red_expr -> red_expr_val
Sourceval reduction_of_red_expr_val : ?occs:(Locus.occurrences * int) -> red_expr_val -> Reductionops.e_reduction_function * Constr.cast_kind

Composition of reduction_of_red_expr_val with eval_red_expr

true if we should use the vm to verify the reduction

Sourceval declare_reduction : string -> Reductionops.reduction_function -> unit

Adding a custom reduction (function to be use at the ML level) NB: the effect is permanent.

Sourceval declare_red_expr : bool -> string -> red_expr -> unit

Adding a custom reduction (function to be called a vernac command). The boolean flag is the locality.

Opaque and Transparent commands.

Sourceval set_strategy : bool -> (Conv_oracle.level * Evaluable.t list) list -> unit

Sets the expansion strategy of a constant. When the boolean is true, the effect is non-synchronous (i.e. it does not survive section and module closure).

call by value normalisation function using the virtual machine

subst_red_expr sub c performs the substitution sub on all kernel names appearing in c

Sourcemodule Intern : sig ... end
Sourcemodule Interp : sig ... end
Sourceval interp_redexp_no_ltac : Environ.env -> Evd.evar_map -> raw_red_expr -> Evd.evar_map * red_expr
Sourcemodule User : sig ... end