functor (T : TermInner.S) (Arg : ARG) (State : sig type t end) ->
  sig
    type term = T.t
    type ty = T.t
    type t
    type dispatch = {
      do_term :
        Traversal.Make.t ->
        depth:int -> Traversal.Make.term -> Traversal.Make.term;
      do_goal_or_axiom :
        (Traversal.Make.t ->
         depth:int ->
         [ `Axiom | `Goal ] -> Traversal.Make.term -> Traversal.Make.term)
        option;
      do_def :
        Traversal.Make.t ->
        depth:int ->
        (Traversal.Make.term, Traversal.Make.ty) Statement.rec_def ->
        Arg.t -> (Traversal.Make.term, Traversal.Make.ty) Statement.rec_def;
      do_pred :
        Traversal.Make.t ->
        depth:int ->
        [ `Not_wf | `Wf ] ->
        [ `Copred | `Pred ] ->
        (Traversal.Make.term, Traversal.Make.ty) Statement.pred_def ->
        Arg.t -> (Traversal.Make.term, Traversal.Make.ty) Statement.pred_def;
      do_copy :
        (Traversal.Make.t ->
         depth:int ->
         loc:Location.t option ->
         (Traversal.Make.term, Traversal.Make.ty) Statement.copy ->
         Arg.t -> (Traversal.Make.term, Traversal.Make.ty) Statement.copy)
        option;
      do_spec :
        (Traversal.Make.t ->
         depth:int ->
         loc:Location.t option ->
         ID.t ->
         (Traversal.Make.term, Traversal.Make.ty) Statement.spec_defs ->
         Arg.t ->
         (Traversal.Make.term, Traversal.Make.ty) Statement.spec_defs)
        option;
      do_data :
        (Traversal.Make.t ->
         depth:int ->
         [ `Codata | `Data ] ->
         Traversal.Make.term Statement.tydef ->
         Arg.t -> Traversal.Make.term Statement.tydef)
        option;
      do_ty_def :
        (Traversal.Make.t ->
         ?loc:Location.t ->
         attrs:Statement.decl_attr list ->
         ID.t ->
         ty:Traversal.Make.ty ->
         Arg.t -> ID.t * Traversal.Make.ty * Statement.decl_attr list)
        option;
    }
    val create :
      ?size:int ->
      ?max_depth:int ->
      env:(Traversal.Make.term, Traversal.Make.ty) Env.t ->
      state:State.t ->
      dispatch:Traversal.Make.dispatch -> unit -> Traversal.Make.t
    val env :
      Traversal.Make.t -> (Traversal.Make.term, Traversal.Make.ty) Env.t
    val state : Traversal.Make.t -> State.t
    val has_processed : Traversal.Make.t -> ID.t -> Arg.t -> bool
    val mark_processed : Traversal.Make.t -> ID.t -> Arg.t -> unit
    val processed : Traversal.Make.t -> (ID.t * Arg.t) Sequence.t
    val call_dep : Traversal.Make.t -> depth:int -> ID.t -> Arg.t -> unit
    exception CannotTraverse
    val traverse_stmt :
      ?after_env:((Traversal.Make.term, Traversal.Make.ty) Env.t -> unit) ->
      Traversal.Make.t ->
      (Traversal.Make.term, Traversal.Make.ty) Statement.t -> unit
    val get_statements :
      Traversal.Make.t ->
      (Traversal.Make.term, Traversal.Make.ty) Statement.t CCVector.vector
    val max_depth_reached : Traversal.Make.t -> bool
  end