Module Logtk.VarSource

Variable

A Variable is a pair of a unique ID.t, and a type.

It is used in TypedSTerm.t for manipulating free and bound variables.

Sourcetype +'a t = private {
  1. id : ID.t;
  2. ty : 'a;
}
Sourcetype 'a var = 'a t
Sourceval make : ty:'a -> ID.t -> 'a t
Sourceval of_string : ty:'a -> string -> 'a t

Make a fresh ID before calling make

Sourceval makef : ty:'a -> ('b, Format.formatter, unit, 'a t) format4 -> 'b
Sourceval gensym : ty:'a -> unit -> 'a t
Sourceval copy : 'a t -> 'a t

copy v is similar to v but with a fresh ID

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

Make a fresh variable with a new type and same ID

Sourceval id : _ t -> ID.t
Sourceval ty : 'a t -> 'a
Sourceval name : _ t -> string
Sourceval compare : _ t -> _ t -> int
Sourceval equal : _ t -> _ t -> bool
Sourceval hash : _ t -> int
Sourceval to_string : _ t -> string
Sourceval pp_full : _ t CCFormat.printer
Sourceval pp_fullc : _ t CCFormat.printer

With color

Sourcemodule Set : sig ... end
Sourcemodule Subst : sig ... end