package coq-core

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

Module CClosure.RedFlagsSource

Sets of reduction kinds.

Sourcetype reds
Sourcetype red_kind
The different kinds of reduction
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.

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