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 Logtk.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