Module TermMono.Var

module Var: Var

type id = ID.t

type 'ty t = private {

	`id : id;`
	`ty : 'ty;`

}

val equal : 'a t -> 'a t -> bool

Equality, purely by identifier. It is impossible to forge two variables with the same identifier but distinct types

val compare : 'a t -> 'a t -> int

Total order based on Var.id

val make : ty:'ty -> name:string -> 'ty t

make ~ty ~name makes a new variable with the given name and type. It will have a unique identifier

val makef : ty:'ty -> ('b, Format.formatter, unit, 'ty t) Pervasives.format4 -> 'b

printf-ready make function

val fresh_copy : 'ty t -> 'ty t

fresh_copy v makes a variable that looks like v but has a fresh identifier

val fresh_copies : 'ty t list -> 'ty t list

Fresh copy each element of the list

val of_id : ty:'ty -> id -> 'ty t

of_id ~ty id makes a variable with the given ID

val ty : 'ty t -> 'ty

val id : 'a t -> id

val name : 'a t -> string

val update_ty : 'a t -> f:('a -> 'b) -> 'b t

Update the type, and make a new variable with it with THE SAME ID. Careful not to break invariants.

val set_ty : 'a t -> ty:'b -> 'b t

Change the type of the variable

val fresh_update_ty : 'a t -> f:('a -> 'b) -> 'b t

Update the type, and make a new variable with it with a fresh ID.

val make_gen : names:(int -> string, unit, string) Pervasives.format -> 'a -> 'a t

make_gen ~names creates a new generator of fresh variables whose names follow the naming scheme names (a formatter with one "%d")

val print : 'a t CCFormat.printer

val to_string : 'a t -> string

val print_full : 'a t CCFormat.printer

val to_string_full : 'a t -> string

Substitutions

module Subst: sig .. end

module Set (Ty : sig
type t 

end) : CCSet.S  with type elt = Ty.t t