package rocq-runtime

  1. Overview
  2. Docs

Module type Trie.SSource

A trie is a generalization of the map data structure where the keys are themselves lists.

Sourcetype label

Keys of the trie structure are label list.

Sourcetype data

Data on nodes of tries are finite sets of data.

Sourcetype t

The trie data structure. Essentially a finite map with keys label list and content data Set.t.

Sourceval empty : t

The empty trie.

Sourceval get : t -> data

Get the data at the current node.

Sourceval next : t -> label -> t

next t lbl returns the subtrie of t pointed by lbl.

Sourceval labels : t -> label list

Get the list of defined labels at the current node.

Sourceval add : label list -> data -> t -> t

add t path v adds v at path path in t.

Sourceval remove : label list -> data -> t -> t

remove t path v removes v from path path in t.

Sourceval iter : (label list -> data -> unit) -> t -> unit

Apply a function to all contents.