Bound

Manipulating user terms

substitute

isClosed

closed

Scopes introduce bound variables

data Scope b f a

Abstraction over bound variables

abstract

abstract1

Instantiation of bound variables

instantiate

instantiate1

Structures permitting substitution

class Bound t

(=<<<)

Conversion to Traditional de Bruijn

data Var b a

fromScope

toScope