package coq

You can search for identifiers within the package.

in-package search v0.2.0

Formal proof management system

Install

Dune Dependency

coq.inria.fr Edit opam file Versions (38)

Authors

T

The Coq development team, INRIA, CNRS, and contributors.

Maintainers

C

coqdev@inria.fr

Sources

coq-8.14.0.tar.gz

sha256=b1501d686c21836302191ae30f610cca57fb309214c126518ca009363ad2cd3c

doc/coq-core.tactics/Dnet/Make/index.html

Module `Dnet.Make`Source

Parameters

module T : Datatype

module Ident : Set.OrderedType

module Meta : Set.OrderedType

Signature

Sourcetype t

Sourcetype ident = Ident.t

provided identifier type

Sourcetype meta = Meta.t

provided metavariable type

Sourcetype 'a structure = 'a T.t

provided parametrized datastructure

Sourcemodule Idset : Set.S with type elt = ident

returned sets of solutions

Sourcetype term_pattern =

| Term of term_pattern structure
| Meta of meta

a pattern is a term where each node can be a unification variable

Sourceval empty : t

Sourceval add : t -> term_pattern -> ident -> t

add t w i adds a new association (w,i) in t.

Sourceval find_all : t -> Idset.t

find_all t returns all identifiers contained in t.

Source

val fold_pattern : 
  ('a -> (Idset.t * meta * t) -> 'a) ->
  'a ->
  term_pattern ->
  t ->
  Idset.t option * 'a

fold_pattern f acc p dn folds f on each meta of p, passing the meta and the sub-dnet under it. The result includes:

Some set if identifiers were gathered on the leafs of the term
None if the pattern contains no leaf (only Metas at the leafs).

Sourceval find_match : term_pattern -> t -> Idset.t

find_match p t returns identifiers of all terms matching p in t.

Sourceval inter : t -> t -> t

set operations on dnets

Sourceval union : t -> t -> t

Sourceval map : (ident -> ident) -> (unit structure -> unit structure) -> t -> t

apply a function on each identifier and node of terms in a dnet

Sourceval map_metas : (meta -> meta) -> t -> t

On This Page

Parameters
Signature