Up – coq » Btermdn

Module `Btermdn`

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 : functor (Z : Stdlib.Map.OrderedType) -> sig ... end

val dnet_depth : int Stdlib.ref