Module LogtkScopedTerm.DB

module DB: sig .. end

type env = LogtkScopedTerm.t LogtkDBEnv.t 
val closed : LogtkScopedTerm.t -> bool
check whether the term is closed (all DB vars are bound within the term). If this returns true then the term doesn't depend on its environment.
val contains : LogtkScopedTerm.t -> int -> bool
Does t contains the De Bruijn variable of index n?
val open_vars : LogtkScopedTerm.t -> LogtkScopedTerm.t Sequence.t
Deprecated.since 0.5.2, dangerous, use LogtkDBEnv functions instead
List of "open" De Bruijn variables (with too high an index)
val shift : int -> LogtkScopedTerm.t -> LogtkScopedTerm.t
shift the non-captured De Bruijn indexes in the term by n
val unshift : int -> LogtkScopedTerm.t -> LogtkScopedTerm.t
unshift n t unshifts the term t's bound variables by n. In other words it decrements indices of all free De Bruijn variables inside by n. Variables bound within t are left untouched.
val replace : LogtkScopedTerm.t -> sub:LogtkScopedTerm.t -> LogtkScopedTerm.t
db_from_term t ~sub replaces sub by a fresh De Bruijn index in t.
val from_var : LogtkScopedTerm.t -> var:LogtkScopedTerm.t -> LogtkScopedTerm.t
db_from_var t ~var replace var by a De Bruijn symbol in t. Same as LogtkScopedTerm.DB.replace.
val eval : env -> LogtkScopedTerm.t -> LogtkScopedTerm.t
Evaluate the term in the given De Bruijn environment, by replacing De Bruijn indices by their value in the environment.