package logtk

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.

Does t contains the De Bruijn variable of index n?

List of "open" De Bruijn variables (with too high an index)

• deprecated

  since 0.5.2, dangerous, use LogtkDBEnv functions instead

shift the non-captured De Bruijn indexes in the term by n

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.

db_from_term t ~sub replaces sub by a fresh De Bruijn index in t.

db_from_var t ~var replace var by a De Bruijn symbol in t. Same as replace.

Evaluate the term in the given De Bruijn environment, by replacing De Bruijn indices by their value in the environment.