disjuncts : term -> term list

SYNOPSIS

Iteratively breaks apart a disjunction.

DESCRIPTION

If a term t is a disjunction p \/ q, then disjuncts t will recursively break down p and q into disjuncts 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 disjunction, the list returned will be [t1; ...; tn]. But

   disjuncts(list_mk_disj([t1;...;tn]))

will not return [t1;...;tn] if any of t1,...,tn is a disjunction.

FAILURE CONDITIONS

Never fails, even if the term is not boolean.

EXAMPLE

  # list_mk_disj [`a \/ b`;`c \/ d`;`e \/ f`];;
  val it : term = `(a \/ b) \/ (c \/ d) \/ e \/ f`

  # disjuncts it;;
  val it : term list = [`a`; `b`; `c`; `d`; `e`; `f`]

  # disjuncts `1`;;
  val it : term list = [`1`]

COMMENTS

Because disjuncts splits both the left and right sides of a disjunction, this operation is not the inverse of list_mk_disj. You can also use splitlist dest_disj to split in a right-associated way only.

SEE ALSO

conjuncts, dest_disj, list_mk_disj.