Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
12345678910111213141516171819202122232425262728293031323334353637383940(************************************************************************)(* * 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. *)
val print : t -> Pp.t(** Printing representation *)
module Set : Set.S with type elt = tmodule Map : CMap.ExtS with type key = t and module Set := Set