package coq-core

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

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

type red_expr_val
val out_occurrences : Locus.occurrences_expr -> Locus.occurrences
val out_with_occurrences : 'a Locus.with_occurrences_expr -> 'a Locus.with_occurrences
val eval_red_expr : Environ.env -> red_expr -> red_expr_val
val 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

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

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

val 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.

val 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

val subst_red_expr : Mod_subst.substitution -> red_expr -> red_expr

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

module Intern : sig ... end
module 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