sig
  val t_select : (Term.term -> 'a) -> (Term.term -> 'a) -> Term.term -> 'a
  val t_selecti :
    ('a -> Term.term -> 'b) ->
    ('a -> Term.term -> 'b) -> 'a -> Term.term -> 'b
  val t_map :
    (Term.term -> Term.term) ->
    (Term.term -> Term.term) -> Term.term -> Term.term
  val t_fold :
    ('a -> Term.term -> 'a) ->
    ('a -> Term.term -> 'a) -> 'a -> Term.term -> 'a
  val t_map_fold :
    ('a -> Term.term -> 'a * Term.term) ->
    ('a -> Term.term -> 'a * Term.term) -> 'a -> Term.term -> 'a * Term.term
  val t_all : (Term.term -> bool) -> (Term.term -> bool) -> Term.term -> bool
  val t_any : (Term.term -> bool) -> (Term.term -> bool) -> Term.term -> bool
  val t_map_simp :
    (Term.term -> Term.term) ->
    (Term.term -> Term.term) -> Term.term -> Term.term
  val t_map_sign :
    (bool -> Term.term -> Term.term) ->
    (bool -> Term.term -> Term.term) -> bool -> Term.term -> Term.term
  val t_map_cont :
    ((Term.term -> 'a) -> Term.term -> 'a) ->
    ((Term.term -> 'a) -> Term.term -> 'a) ->
    (Term.term -> 'a) -> Term.term -> 'a
  val tr_map :
    (Term.term -> Term.term) ->
    (Term.term -> Term.term) -> Term.trigger -> Term.trigger
  val tr_fold :
    ('a -> Term.term -> 'a) ->
    ('a -> Term.term -> 'a) -> 'a -> Term.trigger -> 'a
  val tr_map_fold :
    ('a -> Term.term -> 'a * Term.term) ->
    ('a -> Term.term -> 'a * Term.term) ->
    'a -> Term.trigger -> 'a * Term.trigger
end