(************************************************************************) (* * 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) *) (************************************************************************)
(** This module defines existential variables, which are isomorphic to [int]. Nonetheless, casting from an [int] to a variable is deemed unsafe, so that to keep track of such casts, one has to use the provided {!unsafe_of_int}
function. *)
type t (** Type of existential variables. *)
val repr : t -> int (** Recover the underlying integer. *)
val unsafe_of_int : int -> t (** This is not for dummies. Do not use this function if you don't know what you
are doing. *)
val equal : t -> t -> bool (** Equality over existential variables. *)
val compare : t -> t -> int (** Comparison over existential variables. *)
val hash : t -> int (** Hash over existential variables. *)
valprint : t -> Pp.t (** Printing representation *)
module Set : Set.S withtype elt = t
module Map : CMap.ExtS withtype key = t and module Set := Set
¤ Dauer der Verarbeitung: 0.12 Sekunden
(vorverarbeitet)
¤
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.
