ACL2s-interface::ACL2s-interface-utils
Some utilities built into the ACL2s interface.
- (flatten-and l): Given a list of terms representing the conjunction of those terms, recursively flatten any conjunctions inside those terms.
- (conjunction-terms x y): Given two terms, produce the conjunction of them, simplifying if either of the terms has a top-level conjunction.
- (cnf-disjunct-to-or expr): Given a CNF disjunct, convert to an equivalent ACL2s expression by adding 'or.
- (get-hyps expr): Get the hypotheses of an implication, returning nil if the given expression is not an implication.
- (get-conc expr): Get the conclusion of an implication, returning nil if the given expression is not an implication.
