An environment is used to map De Bruijn indices to objects (or nothing).
This is low level and should be used with a lot of care (it's mostly used in InnerTerm.view.DB and a lot of coffee or aspiring at hand.
val empty : 'a tEmpty environment
val is_empty : 'a t -> boolAre there bindings?
val make : int -> 'a tEmpty environment of the given size
val singleton : 'a -> 'a tSingle 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
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.
Invalid_argument if the env is empty
val size : 'a t -> intval find : 'a t -> int -> 'a optionFind to which value the given De Bruijn index is bound to, or return None
val find_exn : 'a t -> int -> 'aUnsafe version of find.
Failure if the index is not bound within env
val mem : _ t -> int -> boolmem 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.
Invalid_argument if the index isn't in the range 0... size-1
val num_bindings : _ t -> intHow many variables are actually bound?
val of_list : (int * 'a) list -> 'a tMap indices to objects
val to_list : 'a t -> 'a option listList of underlying elements
val to_list_i : 'a t -> (int * 'a) option listList of underlying elements
include Interfaces.PRINT1 with type 'a t := 'a tval pp : 'a CCFormat.printer -> 'a t CCFormat.printerval to_string : 'a CCFormat.printer -> 'a t -> string