package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type
val subst_evaluable_reference : Mod_subst.substitution -> Evaluable.t -> Evaluable.t

Here the semantics is completely unclear. What does "Hint Unfold t" means when "t" is a parameter? Does the user mean "Unfold X.t" or does she mean "Unfold y" where X.t is later on instantiated with y? I choose the first interpretation (i.e. an evaluable reference is never expanded).

type reduction_tactic_error =
  1. | InvalidAbstraction of Environ.env * Evd.evar_map * EConstr.constr * Environ.env * Type_errors.type_error
exception ReductionTacticError of reduction_tactic_error
Reduction functions associated to tactics.

Evaluable global reference

val is_evaluable : Environ.env -> Evaluable.t -> bool
exception NotEvaluableRef of Names.GlobRef.t
val error_not_evaluable : ?loc:Loc.t -> Names.GlobRef.t -> 'a
val evaluable_of_global_reference : Environ.env -> Names.GlobRef.t -> Evaluable.t

Fails on opaque constants and variables (both those without bodies and those marked Opaque in the conversion oracle).

val soft_evaluable_of_global_reference : ?loc:Loc.t -> Names.GlobRef.t -> Evaluable.t

Succeeds for any constant or variable even if marked opaque or otherwise not evaluable.

val global_of_evaluable_reference : Evaluable.t -> Names.GlobRef.t
val red_product : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr option

Red (returns None if nothing reducible)

Simpl

Simpl only at the head

Hnf: like whd_simpl but force delta-reduction of constants that do not immediately hide a non reducible fix or cofix

Variant of the above that does not perform nf-βι

Unfold

Fold

Pattern

Rem: Lazy strategies are defined in Reduction

val cbv_norm_flags : RedFlags.reds -> strong:bool -> Reductionops.reduction_function

Call by value strategy (uses Closures)

val cbv_betadeltaiota : Reductionops.reduction_function

= cbv_betadeltaiota

reduce_to_atomic_ind env sigma t puts t in the form t'=(I args) with I an inductive definition; returns I and t' or fails with a user error

reduce_to_quantified_ind env sigma t puts t in the form t'=(x1:A1)..(xn:An)(I args) with I an inductive definition; returns I and t' or fails with a user error

Same as reduce_to_quantified_ind but more efficient because it does not return the normalized type.

val reduce_to_quantified_ref : ?allow_failure:bool -> Environ.env -> Evd.evar_map -> Names.GlobRef.t -> EConstr.types -> EConstr.types

reduce_to_quantified_ref env sigma ref t try to put t in the form t'=(x1:A1)..(xn:An)(ref args). When this is not possible, if allow_failure is specified, t is unfolded until the point where this impossibility is plainly visible. Otherwise, it fails with user error.

val reduce_to_atomic_ref : ?allow_failure:bool -> Environ.env -> Evd.evar_map -> Names.GlobRef.t -> EConstr.types -> EConstr.types
val check_privacy : Environ.env -> Names.inductive -> unit

Errors if the inductive is not allowed for pattern-matching. *

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