sig
  type t =
      Final of int
    | Atom of Sl_heap.t * int
    | Circle of Tl_form.??.t * int
    | Diamond of Tl_form.??.t * int
    | Box of Tl_form.??.t * int
    | AG of Tags.elt * Tl_form.??.t * int
    | EG of Tags.elt * Tl_form.??.t * int
    | AF of Tl_form.??.t * int
    | EF of Tl_form.??.t * int
    | And of Tl_form.??.t list * int
    | Or of Tl_form.??.t list * int
  val compare : t -> t -> int
  val hash : t -> int
  val pp : Format.formatter -> t -> unit
  val is_final : Tl_form.??.t -> bool
  val is_atom : Tl_form.??.t -> bool
  val is_circle : Tl_form.??.t -> bool
  val is_diamond : Tl_form.??.t -> bool
  val is_box : Tl_form.??.t -> bool
  val is_ag : Tl_form.??.t -> bool
  val is_eg : Tl_form.??.t -> bool
  val is_af : Tl_form.??.t -> bool
  val is_ef : Tl_form.??.t -> bool
  val is_and : Tl_form.??.t -> bool
  val is_or : Tl_form.??.t -> bool
  val is_slformula : Tl_form.??.t -> bool
  val is_checkable : Tl_form.??.t -> bool
  val dest_atom : Tl_form.??.t -> Sl_heap.t
  val dest_circle : Tl_form.??.t -> Tl_form.??.t
  val dest_diamond : Tl_form.??.t -> Tl_form.??.t
  val dest_box : Tl_form.??.t -> Tl_form.??.t
  val dest_ag : Tl_form.??.t -> Tags.elt * Tl_form.??.t
  val dest_eg : Tl_form.??.t -> Tags.elt * Tl_form.??.t
  val dest_af : Tl_form.??.t -> Tl_form.??.t
  val dest_ef : Tl_form.??.t -> Tl_form.??.t
  val dest_and : Tl_form.??.t -> Tl_form.??.t list
  val dest_or : Tl_form.??.t -> Tl_form.??.t list
  val mk_final : Tl_form.??.t
  val mk_atom : Sl_heap.t -> Tl_form.??.t
  val mk_circle : Tl_form.??.t -> Tl_form.??.t
  val mk_diamond : Tl_form.??.t -> Tl_form.??.t
  val mk_box : Tl_form.??.t -> Tl_form.??.t
  val mk_ag : Tags.elt -> Tl_form.??.t -> Tl_form.??.t
  val mk_eg : Tags.elt -> Tl_form.??.t -> Tl_form.??.t
  val mk_af : Tl_form.??.t -> Tl_form.??.t
  val mk_ef : Tl_form.??.t -> Tl_form.??.t
  val mk_and : Tl_form.??.t list -> Tl_form.??.t
  val mk_or : Tl_form.??.t list -> Tl_form.??.t
  val unfold_ag : Tl_form.??.t -> Tl_form.??.t * Tl_form.??.t
  val unfold_eg : Tl_form.??.t -> Tl_form.??.t * Tl_form.??.t
  val unfold_af : Tl_form.??.t -> Tl_form.??.t * Tl_form.??.t
  val unfold_ef : Tl_form.??.t -> Tl_form.??.t * Tl_form.??.t
  val unfold_or : Tl_form.??.t -> Tl_form.??.t * Tl_form.??.t
  val unfold_and : Tl_form.??.t -> Tl_form.??.t * Tl_form.??.t
  val to_string : Tl_form.??.t -> string
  val to_melt : Tl_form.??.t -> Latex.t
  val parse : (Tl_form.??.t, 'a) MParser.t
  val of_string : string -> Tl_form.??.t
  val to_slformula : Tl_form.??.t -> Sl_form.t
  val extract_checkable_slformula : Tl_form.??.t -> Sl_form.t
  val tags : Tl_form.??.t -> Tags.t
  val outermost_tag : Tl_form.??.t -> Tags.t
  val subst_tags : Tagpairs.t -> Tl_form.??.t -> Tl_form.??.t
  val vars : Tl_form.??.t -> Sl_term.Set.t
  val equal : Tl_form.??.t -> Tl_form.??.t -> bool
  val equal_upto_tags : Tl_form.??.t -> Tl_form.??.t -> bool
  val complete_tags : Tags.t -> Tl_form.??.t -> Tl_form.??.t
  val e_step : Tl_form.??.t -> Tl_form.??.t
  val a_step : Tl_form.??.t -> Tl_form.??.t
end