package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (3)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.1.0.tar.gz
sha256=b236dc44f92e1eeca6877c7ee188a90c2303497fe7beb99df711ed5a7ce0d824

doc/rocq-runtime.clib/Trie/module-type-S/index.html

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.