module T: sig .. end
type
val view : t -> (t, FO.Ty.t) FO.view
Observe the structure of the term
val compare : t -> t -> int
Fast total ordering on values of type t.
NOT structural comparison!
There is no guarantee that two terms that are only structurally equal,
but that have been built independently, will compare to 0
val equal : t -> t -> bool
val hash : t -> int
val builtin : FO.Builtin.t -> t
val const : FO.id -> t
val app : FO.id -> t list -> t
val data_test : FO.id -> t -> t
val data_select : FO.id -> int -> t -> t
val undefined : FO.id -> t -> t
val undefined_atom : FO.id -> FO.Ty.toplevel_ty -> t list -> t
val unparsable : FO.Ty.t -> t
val var : FO.Ty.t FO.var -> t
val let_ : FO.Ty.t FO.var -> t -> t -> t
val fun_ : FO.Ty.t FO.var -> t -> t
val mu : FO.Ty.t FO.var -> t -> t
val ite : t -> t -> t -> t
val true_ : t
val false_ : t
val eq : t -> t -> t
val and_ : t list -> t
val or_ : t list -> t
val not_ : t -> t
val imply : t -> t -> t
val equiv : t -> t -> t
val forall : FO.Ty.t FO.var -> t -> t
val exists : FO.Ty.t FO.var -> t -> t
val to_seq : t -> t Sequence.t
subterms