X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Fformula.mli;h=69bdb78645a9f63df4bafbad7d581756f04daa34;hp=6c54386e212f43d74dcd4e29d1e315fadfd88d62;hb=09cd270a1d9d1405795aa3d220267bc3141dd0bd;hpb=d0dc6fbd661c7a79a2d8f875a204f587e6a5162d diff --git a/src/formula.mli b/src/formula.mli index 6c54386..69bdb78 100644 --- a/src/formula.mli +++ b/src/formula.mli @@ -53,7 +53,7 @@ val size : t -> int (** Syntactic size of the formula *) val eval_form : (StateSet.t * StateSet.t) -> t -> bool -(** [eval_form sf,sn F] evaluates the formula [F] on [(sf,sn)] *) +(** [eval_form (sf,sn) F] evaluates the formula [F] on [(sf,sn)] *) val infer_form : (StateSet.t * StateSet.t) -> (StateSet.t * StateSet.t) -> t -> bool (** [eval_form S1 S2 F] infers S1; S2 |- F *)