Module `Libzipperposition_induction__.Test_prop`

Test Properties

type term = Logtk.Term.t
type lit = Logtk.Literal.t
type form = Logtk.Literals.t list
type res = | R_ok | R_fail of Logtk.Subst.t

val check_form : ?⁠limit:int -> form -> res

check_form rules form returns R_ok if the property seems to hold up to depth, or R_fail subst if subst makes form evaluate to false

parameter limit: a limit on how many "steps" are done (for some notion of steps). The higher, the more expensive, but also the more accurate this is.

val default_limit : int