package logtk

  1. Overview
  2. Docs
On This Page
  1. Variable
package logtk
Legend:
Library
Module
Module type
Parameter
Class
Class type

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.

  • since 1.5
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