package coq-core

  1. Overview
  2. Docs
The Coq Proof Assistant -- Core Binaries and Tools

Install 

dune-project
 Dependency

coq.inria.fr Readme Edit opam file Versions (11)

Authors

  1. T
    The Coq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Coq development team <coqdev@inria.fr>

Sources

coq-8.17.1.tar.gz
sha512=9a35311acec2a806730b94ac7dceabc88837f235c52a14c026827d9b89433bd7fa9555a9fc6829aa49edfedb24c8bbaf1411ebf463b74a50aeb17cba47745b6b

doc/coq-core.tactics/Redexpr/index.html

Module RedexprSource

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

Sourcetype red_expr_val
Sourceval out_with_occurrences : 'a Locus.with_occurrences -> Locus.occurrences * 'a
Sourceval eval_red_expr : Environ.env -> red_expr -> red_expr_val

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 * Tacred.evaluable_global_reference 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