package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type
type evaluable_global_reference =
  1. | EvalVarRef of Names.Id.t
  2. | EvalConstRef of Names.Constant.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_global_reference -> bool
exception NotEvaluableRef of Names.GlobRef.t
val error_not_evaluable : Names.GlobRef.t -> 'a
val evaluable_of_global_reference : Environ.env -> Names.GlobRef.t -> evaluable_global_reference
val global_of_evaluable_reference : evaluable_global_reference -> Names.GlobRef.t
exception Redelimination

Red (raise user error if nothing reducible)

val try_red_product : Reductionops.reduction_function

Red (raise Redelimination 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

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