type width = int

module type DB = sig
  type t
  val sexp_of_t : t -> Sexplib.Sexp.t
  val equal : t -> t -> bool
  val to_int : t -> int
  val fresh : free:width -> t
end

module Ix : sig
  include DB
  val shift : t -> t
end

module Lv : sig
  include DB
end

val lv_of_ix : free:width -> Ix.t -> Lv.t

val ix_of_lv : free:width -> Lv.t -> Ix.t

module Env : sig
* An environment , to be accessed in a last - in first - out fashion .
  type 'a t

  (** The number of entries in the environment. *)
  val width : 'a t -> width

* [ well_scoped env lv ] checks that the De Bruijn level [ lv ] is well - scoped 
       in [ env ] .
      in [env]. *)
  val well_scoped_lv : 'a t -> Lv.t -> bool

  (** The empty environment. *)
  val empty : 'a t

  (** Extend an environment with a new entry, considered as the latest one. *)
  val extend : 'a -> 'a t -> 'a t

* [ lookup ix env ] returns the value at De Bruijn index [ ix ] in [ env ] . It 
       raises [ Not_found ] if [ ix ] is not well - scoped in [ env ] .
      raises [Not_found] if [ix] is not well-scoped in [env]. *)
  val lookup : Ix.t -> 'a t -> 'a

* [ find p env ] returns the first value satisfying the predicate [ p ] in 
       [ env ] . It raises [ Not_found ] in the absence of such a value .
      [env]. It raises [Not_found] in the absence of such a value. *)
  val find : ('a -> bool) -> 'a t -> Ix.t * 'a

* See { !  } .
  val map : ('a -> 'b) -> 'a t -> 'b t

* See { !  } .
  val fold : ('a -> 'b -> 'b) -> 'a t -> 'b -> 'b

  (** A variant of {! fold} providing easy access to the environment following
      each extension. *)
  val fold_cons : ('a -> 'a t -> 'b -> 'b) -> 'a t -> 'b -> 'b

  (** See {! List.to_seq}. *)
  val to_seq : 'a t -> 'a Seq.t

  val sexp_of_t : ('a -> Sexplib.Sexp.t) -> 'a t -> Sexplib.Sexp.t
end


* The number of entries in the environment. 
* The empty environment. 
* Extend an environment with a new entry, considered as the latest one. 
* A variant of {! fold} providing easy access to the environment following
      each extension. 
* See {! List.to_seq}. 
type width = int

module type DB = sig
  type t
  val sexp_of_t : t -> Sexplib.Sexp.t
  val equal : t -> t -> bool
  val to_int : t -> int
  val fresh : free:width -> t
end

module Ix : sig
  include DB
  val shift : t -> t
end

module Lv : sig
  include DB
end

val lv_of_ix : free:width -> Ix.t -> Lv.t

val ix_of_lv : free:width -> Lv.t -> Ix.t

module Env : sig
* An environment , to be accessed in a last - in first - out fashion .
  type 'a t

  val width : 'a t -> width

* [ well_scoped env lv ] checks that the De Bruijn level [ lv ] is well - scoped 
       in [ env ] .
      in [env]. *)
  val well_scoped_lv : 'a t -> Lv.t -> bool

  val empty : 'a t

  val extend : 'a -> 'a t -> 'a t

* [ lookup ix env ] returns the value at De Bruijn index [ ix ] in [ env ] . It 
       raises [ Not_found ] if [ ix ] is not well - scoped in [ env ] .
      raises [Not_found] if [ix] is not well-scoped in [env]. *)
  val lookup : Ix.t -> 'a t -> 'a

* [ find p env ] returns the first value satisfying the predicate [ p ] in 
       [ env ] . It raises [ Not_found ] in the absence of such a value .
      [env]. It raises [Not_found] in the absence of such a value. *)
  val find : ('a -> bool) -> 'a t -> Ix.t * 'a

* See { !  } .
  val map : ('a -> 'b) -> 'a t -> 'b t

* See { !  } .
  val fold : ('a -> 'b -> 'b) -> 'a t -> 'b -> 'b

  val fold_cons : ('a -> 'a t -> 'b -> 'b) -> 'a t -> 'b -> 'b

  val to_seq : 'a t -> 'a Seq.t

  val sexp_of_t : ('a -> Sexplib.Sexp.t) -> 'a t -> Sexplib.Sexp.t
end

