		Search-engine friendly clone of the ACL2 documentation.

Imf-example

Imf-cst-comments-conc

Signature
(imf-cst-comments-conc cst) → cstss
Arguments: cst — Guard (treep cst).
Returns: cstss — Type (tree-list-listp cstss).

Definitions and Theorems

Function: imf-cst-comments-conc

(defun imf-cst-comments-conc (cst)
  (declare (xargs :guard (treep cst)))
  (declare (xargs :guard (imf-cst-matchp cst "comments")))
  (let ((__function__ 'imf-cst-comments-conc))
    (declare (ignorable __function__))
    (tree-nonleaf->branches cst)))

Theorem: tree-list-listp-of-imf-cst-comments-conc

(defthm tree-list-listp-of-imf-cst-comments-conc
  (b* ((cstss (imf-cst-comments-conc cst)))
    (tree-list-listp cstss))
  :rule-classes :rewrite)

Theorem: imf-cst-comments-conc-match

(defthm imf-cst-comments-conc-match
  (implies (imf-cst-matchp cst "comments")
           (b* ((cstss (imf-cst-comments-conc cst)))
             (imf-cst-list-list-conc-matchp
                  cstss "\"Comments:\" unstructured crlf")))
  :rule-classes :rewrite)

Theorem: imf-cst-comments-conc-of-tree-fix-cst

(defthm imf-cst-comments-conc-of-tree-fix-cst
  (equal (imf-cst-comments-conc (tree-fix cst))
         (imf-cst-comments-conc cst)))

Theorem: imf-cst-comments-conc-tree-equiv-congruence-on-cst

(defthm imf-cst-comments-conc-tree-equiv-congruence-on-cst
  (implies (tree-equiv cst cst-equiv)
           (equal (imf-cst-comments-conc cst)
                  (imf-cst-comments-conc cst-equiv)))
  :rule-classes :congruence)