sig
  type abstract = Existing of int | Fresh of Agent.t
  type 'a port = 'a * int
  type 'a arrow =
      ToNode of 'Navigation.port
    | ToNothing
    | ToInternal of int
  type 'a step = 'Navigation.port * 'Navigation.arrow
  type 'a t = 'Navigation.step list
  val print :
    Signature.s ->
    (int -> int) ->
    Format.formatter -> Navigation.abstract Navigation.t -> unit
  val step_to_yojson :
    Navigation.abstract Navigation.step -> Yojson.Basic.json
  val step_of_yojson :
    Yojson.Basic.json -> Navigation.abstract Navigation.step
  val to_yojson : Navigation.abstract Navigation.t -> Yojson.Basic.json
  val of_yojson : Yojson.Basic.json -> Navigation.abstract Navigation.t
  val rename :
    Renaming.t ->
    Navigation.abstract Navigation.t ->
    Renaming.t * Navigation.abstract Navigation.t
  val compatible_fresh_point :
    Navigation.abstract Navigation.step ->
    Agent.t ->
    int -> Navigation.abstract Navigation.arrow -> Renaming.t option
  val is_subnavigation :
    Renaming.t ->
    Navigation.abstract Navigation.t ->
    Navigation.abstract Navigation.t ->
    (Renaming.t * Navigation.abstract Navigation.t) option
  val check_edge : Edges.t -> Navigation.abstract Navigation.step -> bool
  val injection_for_one_more_edge :
    ?root:Agent.t ->
    Renaming.t ->
    Edges.t -> Navigation.abstract Navigation.step -> Renaming.t option
  val imperative_edge_is_valid :
    ?root:Agent.t ->
    Renaming.t -> Edges.t -> Navigation.abstract Navigation.step -> bool
  val concretize :
    Agent.t ->
    Edges.t -> Navigation.abstract Navigation.t -> int Navigation.t option
end