Module Term.TermTF

module TermTF: sig .. end

val t_select : (Term.term -> 'a) -> (Term.term -> 'a) -> Term.term -> 'a

t_select fnT fnF t is fnT t if t is a value, fnF t otherwise

val t_selecti : ('a -> Term.term -> 'b) -> ('a -> Term.term -> 'b) -> 'a -> Term.term -> 'b

t_selecti fnT fnF acc t is t_select (fnT acc) (fnF acc) t

val t_map : (Term.term -> Term.term) ->
       (Term.term -> Term.term) -> Term.term -> Term.term

t_map fnT fnF = t_map (t_select fnT fnF)

val t_fold : ('a -> Term.term -> 'a) -> ('a -> Term.term -> 'a) -> 'a -> Term.term -> 'a

t_fold fnT fnF = t_fold (t_selecti fnT fnF)

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