1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
|
\DOC disjuncts
\TYPE {disjuncts : term -> term list}
\SYNOPSIS
Iteratively breaks apart a disjunction.
\DESCRIBE
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]))
}
\noindent will not return {[t1;...;tn]} if any of {t1},...,{tn} is a
disjunction.
\FAILURE
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.
\SEEALSO
conjuncts, dest_disj, list_mk_disj.
\ENDDOC
|
