package logtk

  1. Overview
  2. Docs
package logtk
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module InnerTerm.DBSource

Sourcetype env = t DBEnv.t
Sourceval closed : 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.

Sourceval contains : t -> int -> bool

Does t contains the De Bruijn variable of index n?

Sourceval unbound : t -> int list

Return a list of all unbound DB indices in a term

Sourceval shift : ?depth:int -> int -> t -> t

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

Sourceval unshift : ?depth:int -> int -> t -> 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.

Sourceval replace : t -> sub:t -> t

replace t ~sub replaces sub by a fresh De Bruijn index in t. Shifts other De Bruijn indices by 1

Sourceval replace_l : t -> l:t list -> t

N-ary version of replace Shifts other De Bruijn indices by length t

Sourceval from_var : t -> var:t -> t

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

Sourceval eval : env -> t -> t

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