Module Logtk.Var

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.

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

Make a fresh ID before calling make

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

copy v is similar to v but with a fresh ID

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

Make a fresh variable with a new type and same ID

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

With color

module Set : sig ... end
module Subst : sig ... end