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.lib/Stateid/index.html

Module StateidSource

Sourcetype t
Sourceval equal : t -> t -> bool
Sourceval compare : t -> t -> int
Sourcemodule Self : Map.OrderedType with type t = t
Sourcemodule Set : Set.S with type elt = t and type t = Set.Make(Self).t
Sourceval initial : t
Sourceval dummy : t
Sourceval fresh : unit -> t
Sourceval to_string : t -> string
Sourceval print : t -> Pp.t
Sourceval of_int : int -> t
Sourceval to_int : t -> int
Sourceval newer_than : t -> t -> bool
Sourceval add : Exninfo.info -> valid:t -> t -> Exninfo.info
Sourceval get : Exninfo.info -> (t * t) option
Sourcetype exn_info = {
  1. id : t;
  2. valid : t;
}
Sourcetype ('a, 'b) request = {
  1. exn_info : exn_info;
  2. stop : t;
  3. document : 'b;
  4. loc : Loc.t option;
  5. uuid : 'a;
  6. name : string;
}
Sourceval is_valid : doc:int -> t -> bool
Sourceval set_is_valid : (doc:int -> t -> bool) -> unit