An environment that maps De Bruijn indices to values of type 'a.

Empty environment

Are there bindings?

Empty environment of the given size

Single binding

Create a new environment, when entering a scope, where the De Bruijn index 0 is bound to the given value

push_l_same_order env l builds env l0 :: l1 :: … :: env

push_l_rev env l builds env l(n-1) :: … :: l1 :: l0 :: env

Create a new environment, when entering a scope, where the De Bruijn index 0 is bound to nothing.

Call push_none n times (after we've entered n scopes, for instances)

Exit a scope, removing the top binding.

• raises Invalid_argument

  if the env is empty

pop_many env n calls pop env n times

Number of scopes (number of times push or push_none were called to produce the given environment)

Find to which value the given De Bruijn index is bound to, or return None

Unsafe version of find.

• raises Failure

  if the index is not bound within env

mem env i returns true iff find env i returns Some _ rather than None, ie. whether the i-th De Bruijn variable is bound within env

Set the n-th variable to the given objects.

• raises Invalid_argument

  if the index isn't in the range 0... size-1

How many variables are actually bound?

Map bound objects to other bound objects

Map indices to objects

List of underlying elements

List of underlying elements