package rocq-runtime

You can search for identifiers within the package.

in-package search v0.2.0

The Rocq Prover -- Core Binaries and Tools

Install

Dune Dependency

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

Authors

T

The Rocq development team, INRIA, CNRS, and contributors

Maintainers

T

The Rocq development team <coqdev@inria.fr>

Sources

rocq-9.0.0.tar.gz

md5=8d522602d23e7a665631826dab9aa92b

sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be

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

Module type `Heap.S`Source

Sourcetype t

Type of functional heaps

Sourcetype elt

Type of elements

Sourceval empty : t

The empty heap

Sourceval add : elt -> t -> t

add x h returns a new heap containing the elements of h, plus x; complexity $ O(log(n)) $

Sourceval maximum : t -> elt

maximum h returns the maximum element of h; raises EmptyHeap when h is empty; complexity $ O(1) $

Sourceval remove : t -> t

remove h returns a new heap containing the elements of h, except the maximum of h; raises EmptyHeap when h is empty; complexity $ O(log(n)) $

Sourceval iter : (elt -> unit) -> t -> unit

usual iterators and combinators; elements are presented in arbitrary order

Sourceval fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a