sig
  type t =
      Atom of Sl_heap_rho.t * int
    | Next of Tl_form_ltl.??.t * int
    | G of Tags.elt * Tl_form_ltl.??.t * int
    | F of Tl_form_ltl.??.t * int
    | And of Tl_form_ltl.??.t list * int
    | Or of Tl_form_ltl.??.t list * int
  val compare : t -> t -> int
  val hash : t -> int
  val pp : Format.formatter -> t -> unit
  val is_atom : Tl_form_ltl.??.t -> bool
  val is_next : Tl_form_ltl.??.t -> bool
  val is_g : Tl_form_ltl.??.t -> bool
  val is_f : Tl_form_ltl.??.t -> bool
  val is_and : Tl_form_ltl.??.t -> bool
  val is_or : Tl_form_ltl.??.t -> bool
  val is_slformula : Tl_form_ltl.??.t -> bool
  val is_checkable : Tl_form_ltl.??.t -> bool
  val dest_atom : Tl_form_ltl.??.t -> Sl_heap_rho.t
  val dest_next : Tl_form_ltl.??.t -> Tl_form_ltl.??.t
  val dest_g : Tl_form_ltl.??.t -> Tags.elt * Tl_form_ltl.??.t
  val dest_f : Tl_form_ltl.??.t -> Tl_form_ltl.??.t
  val dest_and : Tl_form_ltl.??.t -> Tl_form_ltl.??.t list
  val dest_or : Tl_form_ltl.??.t -> Tl_form_ltl.??.t list
  val mk_atom : Sl_heap_rho.t -> Tl_form_ltl.??.t
  val mk_next : Tl_form_ltl.??.t -> Tl_form_ltl.??.t
  val mk_g : Tags.elt -> Tl_form_ltl.??.t -> Tl_form_ltl.??.t
  val mk_f : Tl_form_ltl.??.t -> Tl_form_ltl.??.t
  val mk_and : Tl_form_ltl.??.t list -> Tl_form_ltl.??.t
  val mk_or : Tl_form_ltl.??.t list -> Tl_form_ltl.??.t
  val unfold_g : Tl_form_ltl.??.t -> Tl_form_ltl.??.t * Tl_form_ltl.??.t
  val unfold_f : Tl_form_ltl.??.t -> Tl_form_ltl.??.t * Tl_form_ltl.??.t
  val unfold_or : Tl_form_ltl.??.t -> Tl_form_ltl.??.t * Tl_form_ltl.??.t
  val unfold_and : Tl_form_ltl.??.t -> Tl_form_ltl.??.t * Tl_form_ltl.??.t
  val to_string : Tl_form_ltl.??.t -> string
  val to_melt : Tl_form_ltl.??.t -> Latex.t
  val parse : (Tl_form_ltl.??.t, 'a) MParser.t
  val of_string : string -> Tl_form_ltl.??.t
  val to_slformula : Tl_form_ltl.??.t -> Sl_form_rho.t
  val extract_checkable_slformula : Tl_form_ltl.??.t -> Sl_form_rho.t
  val tags : Tl_form_ltl.??.t -> Tags.t
  val outermost_tag : Tl_form_ltl.??.t -> Tags.t
  val subst_tags : Tagpairs.t -> Tl_form_ltl.??.t -> Tl_form_ltl.??.t
  val vars : Tl_form_ltl.??.t -> Sl_term.Set.t
  val equal : Tl_form_ltl.??.t -> Tl_form_ltl.??.t -> bool
  val equal_upto_tags : Tl_form_ltl.??.t -> Tl_form_ltl.??.t -> bool
  val complete_tags : Tags.t -> Tl_form_ltl.??.t -> Tl_form_ltl.??.t
  val step : Tl_form_ltl.??.t -> Tl_form_ltl.??.t
end