/usr/share/hol88-2.02.19940316/help/ENTRIES/conjuncts.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 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
|