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)

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`

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