		Search-engine friendly clone of the ACL2 documentation.

Smt-translator

Paragraphp

A paragraph is made up of lists of words. Notice a single word is also counted as a paragraphp.

Signature
(paragraphp par) → paragraph?
Returns: paragraph? — Type (booleanp paragraph?).

Definitions and Theorems

Function: paragraphp

(defun paragraphp (par)
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'paragraphp))
    (declare (ignorable acl2::__function__))
    (if (atom par)
        (wordp par)
      (and (paragraphp (car par))
           (paragraphp (cdr par))))))

Theorem: booleanp-of-paragraphp

(defthm booleanp-of-paragraphp
  (b* ((paragraph? (paragraphp par)))
    (booleanp paragraph?))
  :rule-classes :rewrite)