package coq-core

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

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

type reds

Set of reduction kinds.

type red_kind

Reduction kind.

val fBETA : red_kind
val fDELTA : red_kind
val fMATCH : red_kind
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.

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