Module `Logtk_arbitrary.ArTerm`

Arbitrary Typed Terms and Formulas

type 'a arbitrary = 'a QCheck.arbitrary
type 'a gen = 'a QCheck.Gen.t

val shrink : Logtk.Term.t QCheck.Shrink.t
val default_g : Logtk.Term.t gen
val default_fuel : int -> Logtk.Term.t gen
val default : Logtk.Term.t arbitrary: Default polymorphic term

val default_ho_g : Logtk.Term.t gen
val default_ho : Logtk.Term.t arbitrary: Default polymorphic term, with lambdas

val default_ho_fuel : int -> Logtk.Term.t gen
val ground_g : Logtk.Term.t gen
val ground : Logtk.Term.t arbitrary: Default ground monomorphic term

val pred : Logtk.Term.t arbitrary: predicates (type "o")

val pos : Logtk.Term.t -> Logtk.Position.t gen: Random valid position in the term

S Terms

module PT : sig ... end