strip_disj

boolSyntax.strip_disj : term -> term list

Recursively breaks apart disjunctions.

If M is of the form t1 \/ ... \/ tn, where no ti is a disjunction, then strip_disj M returns [t1,...,tn]. Any ti that is a disjunction is broken down by strip_disj, hence

   strip_disj(list_mk_disj [t1,...,tn])

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

Failure

Never fails.

Example

> strip_disj (Term `(a \/ b) \/ c \/ d`);
val it = [“a”, “b”, “c”, “d”]: term list

See also

boolSyntax.dest_disj, boolSyntax.mk_disj, boolSyntax.list_mk_disj