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.0.1.tar.gz
sha256=051f7bf702ff0a3b370449728921e5a95e18bc2b31b8eb949d48422888c98af4

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

Module type Store.SSource

Sourcetype t

Type of stores

Sourcetype 'a field

Type of field of such stores

Sourceval field : string -> 'a field

Create a new field. See also Dyn.create.

Sourceval empty : t

Empty store

Sourceval set : t -> 'a field -> 'a -> t

Set a field

Sourceval get : t -> 'a field -> 'a option

Get the value of a field, if any

Sourceval remove : t -> 'a field -> t

Unset the value of the field

Sourceval merge : t -> t -> t

merge s1 s2 adds all the fields of s1 into s2.