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
44
45
|
\DOC disjuncts
\TYPE {disjuncts : (term -> term list)}
\SYNOPSIS
Iteratively breaks apart a disjunction.
\DESCRIBE
{disjuncts "t1 \/ ... \/ tn"} returns {["t1";...;"tn"]}.
The argument term may be any tree of disjunctions;
it need not have the form {"t1 \/ (t2 \/ ( ... \/ tn)...)"}.
A term that is not a disjunction is simply returned as the sole element of a
list. Note that
{
disjuncts(list_mk_disj(["t1";...;"tn"]))
}
\noindent will not return {["t1";...;"tn"]} if any of {t1},...,{tn} are
disjunctions.
\FAILURE
Never fails.
\EXAMPLE
{
#list_mk_disj ["a \/ b";"c \/ d";"e \/ f"];;
"(a \/ b) \/ (c \/ d) \/ e \/ f" : term
#disjuncts it;;
["a"; "b"; "c"; "d"; "e"; "f"] : term list
#list_mk_disj it;;
"a \/ b \/ c \/ d \/ e \/ f" : term
#disjuncts "1";;
["1"] : term list
}
\COMMENTS
Because {disjuncts} splits both the left and right sides of a disjunction,
this operation is not the inverse of {list_mk_disj}. It may be useful to
introduce {list_dest_disj} for splitting only the right tails of a disjunction.
\SEEALSO
list_mk_disj, dest_disj.
\ENDDOC
|
