val term_of_value: value -> CicNotationPt.term
val well_typed: value_type -> value -> bool
+val declarations_of_env: t -> declaration list
+
(** {2 Environment lookup} *)
val lookup_value: t -> string -> value
val lookup_string: t -> string -> string
val lookup_term: t -> string -> CicNotationPt.term
+val remove: t -> string -> t
+
(** {2 Bindings mangling} *)
val opt_binding_some: binding -> binding (* v -> Some v *)
val opt_declaration: declaration -> declaration (* t -> OptType t *)
val list_declaration: declaration -> declaration (* t -> ListType t *)
+(** given a list of environments bindings a set of names n_1, ..., n_k, returns
+ * a single environment where n_i is bound to the list of values bound in the
+ * starting environments *)
+val coalesce_env: declaration list -> t list -> t
+