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