package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type reds
type red_kind
The different kinds of reduction
val fBETA : red_kind
val fDELTA : red_kind
val fETA : red_kind

The fETA flag is never used by the kernel reduction but pretyping does

val fMATCH : red_kind

The fETA flag is never used by the kernel reduction but pretyping does

val fFIX : red_kind
val fCOFIX : red_kind
val fZETA : red_kind
val fCONST : Names.Constant.t -> red_kind
val fVAR : Names.Id.t -> red_kind
val no_red : reds

No reduction at all

val red_add : reds -> red_kind -> reds

Adds a reduction kind to a set

val red_sub : reds -> red_kind -> reds

Removes a reduction kind to a set

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

Adds a reduction kind to a set

val red_transparent : reds -> TransparentState.t

Retrieve the transparent state of the reduction flags

val mkflags : red_kind list -> reds

Build a reduction set from scratch = iter red_add on no_red

val red_set : reds -> red_kind -> bool

Tests if a reduction kind is set

val 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