logtk

Core types and algorithms for logic
IN THIS PACKAGE
Module Logtk . Term . DB

De Bruijn

val is_closed : t -> bool
val shift : ?depth:int -> int -> t -> t
val unshift : ?depth:int -> int -> t -> t
val eval : t DBEnv.t -> t -> t
val unbound : t -> int list
val skolemize_loosely_bound : ?already_sk:t IntMap.t -> t -> t * t IntMap.t
val unskolemize : int Map.t -> Map.key -> t
val map_vars_shift : ?depth:int -> int Map.t -> t -> t