package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (3)

Authors

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

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.1.0.tar.gz
sha256=b236dc44f92e1eeca6877c7ee188a90c2303497fe7beb99df711ed5a7ce0d824

doc/rocq-runtime.pretyping/Tacred/index.html

Module TacredSource

Sourceval 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).

Sourcetype reduction_tactic_error =
  1. | InvalidAbstraction of Environ.env * Evd.evar_map * EConstr.constr * Environ.env * Type_errors.type_error
Sourcetype 'a change =
  1. | NoChange
  2. | Changed of 'a
Sourceexception ReductionTacticError of reduction_tactic_error
Reduction functions associated to tactics.

Evaluable global reference

Sourceval is_evaluable : Environ.env -> Evaluable.t -> bool
Sourceexception NotEvaluableRef of Names.GlobRef.t
Sourceval error_not_evaluable : ?loc:Loc.t -> Names.GlobRef.t -> 'a
Sourceval 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).

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

Sourceval global_of_evaluable_reference : Evaluable.t -> Names.GlobRef.t

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

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

Call by value strategy (uses Closures)

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

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

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

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