package coq-core

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

Module RedFlagsSource

Delta implies all consts (both global (= by kernel_name) and local (= by Rel or Var)), all evars, and letin's. Rem: reduction of a Rel/Var bound to a term is Delta, but reduction of a LetIn expression is Letin reduction

Sourcetype reds

Set of reduction kinds.

Sourcetype red_kind

Reduction kind.

Sourceval fBETA : red_kind
Sourceval fDELTA : red_kind
Sourceval fMATCH : red_kind
Sourceval fFIX : red_kind
Sourceval fCOFIX : red_kind
Sourceval fZETA : red_kind
Sourceval no_red : reds

No reduction at all

Sourceval red_add : reds -> red_kind -> reds

Adds a reduction kind to a set

Sourceval red_sub : reds -> red_kind -> reds

Removes a reduction kind to a set

Sourceval red_add_transparent : reds -> TransparentState.t -> reds

Adds a reduction kind to a set

Sourceval red_transparent : reds -> TransparentState.t

Retrieve the transparent state of the reduction flags

Sourceval mkflags : red_kind list -> reds

Build a reduction set from scratch = iter red_add on no_red

Sourceval red_set : reds -> red_kind -> bool

Tests if a reduction kind is set

Sourceval red_projection : reds -> Names.Projection.t -> bool

This tests if the projection is in unfolded state already or is unfodable due to delta.

Sourceval all : reds
Sourceval allnolet : reds
Sourceval beta : reds
Sourceval betadeltazeta : reds
Sourceval betaiota : reds
Sourceval betaiotazeta : reds
Sourceval betazeta : reds
Sourceval delta : reds
Sourceval zeta : reds
Sourceval nored : reds
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