(************************************************************************) (* * The Rocq Prover / The Rocq Development Team *) (* v * Copyright INRIA, CNRS and contributors *) (* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (* * (see LICENSE file for the text of the license) *) (************************************************************************)
module type S = sig
type node
module NodeSet : Set.S withtype elt = node
type ('edge,'info,'cdata) t
val empty : ('e,'i,'d) t
val add_edge : ('e,'i,'d) t -> node -> 'e -> node -> ('e,'i,'d) t val from_node : ('e,'i,'d) t -> node -> (node * 'e) list val mem : ('e,'i,'d) t -> node -> bool val del_edge : ('e,'i,'d) t -> node -> node -> ('e,'i,'d) t val del_nodes : ('e,'i,'d) t -> NodeSet.t -> ('e,'i,'d) t val all_nodes : ('e,'i,'d) t -> NodeSet.t
val get_info : ('e,'i,'d) t -> node -> 'i option val set_info : ('e,'i,'d) t -> node -> 'i -> ('e,'i,'d) t val clear_info : ('e,'i,'d) t -> node -> ('e,'i,'d) t
(* A property applies to a set of nodes and holds some data. Stm uses this feature to group nodes contributing to the same proofs and
to structure proofs in boxes limiting the scope of errors *)
module Property : sig type'd t val equal : 'd t -> 'd t -> bool val compare : 'd t -> 'd t -> int val to_string : 'd t -> string val data : 'd t -> 'd val having_it : 'd t -> NodeSet.t end
val create_property : ('e,'i,'d) t -> node list -> 'd -> ('e,'i,'d) t val property_of : ('e,'i,'d) t -> node -> 'd Property.t list val del_property : ('e,'i,'d) t -> 'd Property.t -> ('e,'i,'d) t
val iter : ('e,'i,'d) t ->
(node -> 'd Property.t list -> 'i option ->
(node * 'e) list -> unit) -> unit
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
