conjuncts : term -> term list
Iteratively breaks apart a conjunction.
If a term t is a conjunction p /\ q, then conjuncts t will recursively
break down p and q into conjuncts and append the resulting lists. Otherwise
it will return the singleton list [t]. So if t is of the form
t1 /\ ... /\ tn with any reassociation, no ti itself being a conjunction,
the list returned will be [t1; ...; tn]. But
will not return [t1;...;tn] if any of t1,...,tn is a
- FAILURE CONDITIONS
Never fails, even if the term is not boolean.
# conjuncts `((p /\ q) /\ r) /\ ((p /\ s /\ t) /\ u)`;;
val it : term list = [`p`; `q`; `r`; `p`; `s`; `t`; `u`]
# conjuncts(list_mk_conj [`a /\ b`; `c:bool`; `d /\ e /\ f`]);;
val it : term list = [`a`; `b`; `c`; `d`; `e`; `f`]
Because conjuncts splits both the left and right sides of a conjunction,
this operation is not the inverse of list_mk_conj. You can also use
splitlist dest_conj to split in a right-associated way only.
- SEE ALSO
dest_conj, disjuncts, is_conj.