		Search-engine friendly clone of the ACL2 documentation.

Convenience-constructors

Pfdef

Construct a definition with zero or more constraints.

Each of the constraints arguments of this macro may be either (a term returning) a single constraint or (a term returning) a list of constraints.

Macro: pfdef

(defmacro pfdef (defname params &rest constraints)
 (cons
  'make-definition
  (cons
   ':name
   (cons
    defname
    (cons
       ':para
       (cons params
             (cons ':body
                   (cons (cons 'pfdef-join
                               (cons (cons 'list constraints) 'nil))
                         'nil))))))))

Definitions and Theorems

Function: pfdef-join

(defun pfdef-join (list)
  (declare (xargs :guard (constraint/constraintlist-listp list)))
  (let ((__function__ 'pfdef-join))
    (declare (ignorable __function__))
    (b* (((when (endp list)) nil)
         (first (car list)))
      (cond ((constraintp first)
             (cons first (pfdef-join (cdr list))))
            ((constraint-listp first)
             (append first (pfdef-join (cdr list))))
            (t (acl2::impossible))))))

Theorem: constraint-listp-of-pfdef-join

(defthm constraint-listp-of-pfdef-join
  (b* ((constrs (pfdef-join list)))
    (constraint-listp constrs))
  :rule-classes :rewrite)