Returns a list of the atomic propositions in a Boolean term
DESCRIPTION
When applied to a term of Boolean type, atoms returns a list of the atomic
fomulas, considering the term as a propositional formula built up recursively
with negation, conjunction, disjunction, implication and logical equivalence,
treating all other subterms (e.g. quantified ones) as atomic.
FAILURE CONDITIONS
Fails if the term does not have type :bool.
EXAMPLE
Here the atomic formulas are simply variables:
# atoms `p \/ q ==> r`;;
val it : term list = [`r`; `p`; `q`]
while here the atomic formulas are composite:
# atoms `x < 1 \/ x > 1 ==> ~(x = 1)`;;
val it : term list = [`x < 1`; `x > 1`; `x = 1`]