Module AltErgoLib.Var

type t
include Container_types.S_plus_stdlib with type t := t
module T : Container_types_intf.Thing with type t = t
include Container_types_intf.Thing with type t := T.t
include Stdlib.Hashtbl.HashedType with type t := T.t
val equal : T.t -> T.t -> bool
val hash : T.t -> int
include Stdlib.Map.OrderedType with type t := T.t
val compare : T.t -> T.t -> int
val print : T.t Fmt.t
module Map : Container_types_intf.Map_plus_stdlib with type key = t and module Set = Set
val of_hstring : Hstring.t -> t

Create a *fresh* variable with the given name.

Calling of_hstring twice with the same Hstring.t as argument will result in *distinct* variables.

val of_string : string -> t

Convenient alias for of_hstring (Hstring.make s).

val local : string -> t

Create a new "local" variable. Local variables are variables used exclusively in user-defined theories for semantic triggers, and are implicitly bound at the level of the enclosing quantifier.

val is_local : t -> bool

Indicates whether the given variable is a local variable (see local above for details).

val uid : t -> int

Globally unique identifier for the variable.

val underscore : t

Unique special variable. Used to indicate fields that should be ignored in pattern matching and triggers.

val to_string : t -> string
val save_cnt : unit -> unit

Saves the values of the counter

val reinit_cnt : unit -> unit

Reinitializes the counter to the saved value with save_cnt, 1 if no value is saved, since after the initialization of the modules cnt is set to 1 when initializing the underscore constant in the Symbols module