Red#

Ltac2.Std.Red

type delta_red

List of references to delta-reduce.

val only : reference list -> delta_red

Limits delta unfolding to the listed constants.

val except : reference list -> delta_red

Limits delta unfolding to all but the listed constants.

val all : delta_red

Does not limit delta unfolding. Equivalent to except [].

type red_flag

A reduction flag.

val head : red_flag

Does only head reduction, without going under binders.

val beta : red_flag

Beta-reduction of functional application.

val delta : delta_red -> red_flag

Delta-reduction: unfolding of transparent constants.

val match_ : red_flag

Reduction of match expressions.

val fix : red_flag

Reduction of fix expressions.

val cofix : red_flag

Reduction of cofix expressions.

val iota : red_flag list

Iota-reduction of pattern-matching (match) over a constructed term and reduction of fix and cofix expressions. Shorthand for [match; fix; cofix].

val zeta : red_flag

Zeta-reduction: reduction of let-in definitions.

val all_flags : head:bool -> red_flag list

All reduction flags.

  • parameter head

    Whether to perform head reduction or not.

Type representing a reduction expression. Red expressions describe which reduction strategy to apply during tactic execution.

val red : t

red βδζι-reduces the head constant of the term, if possible.

val hnf : t

hnf reduces the goal to its weak-head normal form: it reduces the head of the goal until it becomes a product or an irreducible term.

val simpl : ?where:(pattern * int Syntax.occurrences) -> red_flag list -> t Proofview.tactic

simpl ?where flags reduces a term to something still readable instead of fully normalizing it. It performs a sort of strong normalization with two key differences:

  • It unfolds constants only if they lead to an ι-reduction, i.e., reducing a match or unfolding a fixpoint.
  • When reducing a constant unfolding to (co)fixpoints, the tactic uses the name of the constant the (co)fixpoint comes from instead of the (co)fixpoint definition in recursive calls.
val cbv : red_flag list -> t Proofview.tactic

cbv flags normalizes the goal as specified by flags.

val cbn : red_flag list -> t Proofview.tactic

cbn flags was intended to be a more principled, faster and more predictable replacement for simpl. The main difference is that cbn may unfold constants even when they cannot be reused in recursive calls.

val lazy_ : red_flag list -> t Proofview.tactic

lazy_ flags performs on-demand reduction using a lazy strategy, only reducing subterms that are needed for the goal, with the given reduction flags.

val unfold : (reference * int Syntax.occurrences) list -> t Proofview.tactic

unfold refs replaces each occurrence of the specified global references by their definitions in the goal.

val fold : constr list -> t

fold cs replaces the specified terms by the given subterms in the goal. This is the inverse of unfold: it introduces β-redexes to fold subterms back.

val pattern : (constr * int Syntax.occurrences) list -> t

pattern cs introduces β-redexes in the goal so that the specified subterms become separate variables at the head of the term.

val vm : ?where:(pattern * int Syntax.occurrences) -> unit -> t

vm ?where () uses the virtual machine for very fast computation, with an optional reduction context.

val native : ?where:(pattern * int Syntax.occurrences) -> unit -> t

native ?where () uses native code compilation for the fastest possible computation, with an optional reduction context.