package coq-core

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

Discrimination nets with bounded depth.

This module registers actions (typically tactics) mapped to patterns

Patterns are stocked linearly as the list of its node in prefix order in such a way patterns having the same prefix have this common prefix shared and the seek for the action associated to the patterns that a term matches are found in time proportional to the maximal number of nodes of the patterns matching the term. The TransparentState.t indicates which constants and variables can be considered as rigid. These dnets are able to cope with existential variables as well, which match Everything.

module Make (Z : Stdlib.Map.OrderedType) : sig ... end
val dnet_depth : int Stdlib.ref
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