package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module RedexprSource

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

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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct