/usr/share/hol88-2.02.19940316/help/ENTRIES/disjuncts.doc is in hol88-help 2.02.19940316-35.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
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
|