		Search-engine friendly clone of the ACL2 documentation.

Defconstrained-recognizer-implementation

Defconstrained-recognizer-fn

Event generated by defconstrained-recognizer.

Signature
(defconstrained-recognizer-fn name nonempty) → event
Returns: event — Type (acl2::maybe-pseudo-event-formp event).

Definitions and Theorems

Function: defconstrained-recognizer-fn

(defun defconstrained-recognizer-fn (name nonempty)
 (declare (xargs :guard t))
 (let ((__function__ 'defconstrained-recognizer-fn))
  (declare (ignorable __function__))
  (b*
   (((unless (symbolp name))
     (raise
      "The NAME input must be a symbol, ~
                but it is ~x0 instead."
      name))
    ((unless (symbolp nonempty))
     (raise
      "The :NONEMPTY input must be a symbol, ~
                but it is ~x0 instead."
      nonempty))
    (pkg (symbol-package-name name))
    (pkg (if (equal pkg *main-lisp-package-name*)
             "ACL2"
           pkg))
    (pkg-witness (pkg-witness pkg))
    (x (intern-in-package-of-symbol "X" pkg-witness))
    (name-sig (cons (cons name '(*)) '(acl2::=> *)))
    (nonempty-sig? (and nonempty
                        (list (cons (cons nonempty 'nil)
                                    '(acl2::=> *)))))
    (name-def
     (cons
      'local
      (cons
       (cons
          'defun
          (cons name
                (cons (cons x 'nil)
                      (cons (cons 'declare
                                  (cons (cons 'ignore (cons x 'nil))
                                        'nil))
                            '(t)))))
       'nil)))
    (nonempty-def?
     (and nonempty
          (list (cons 'local
                      (cons (cons 'defun (cons nonempty '(nil nil)))
                            'nil)))))
    (booleanp-of-name
     (cons
      'defthm
      (cons (acl2::packn-pos (list 'booleanp-of- name)
                             pkg-witness)
            (cons (cons 'booleanp
                        (cons (cons name (cons x 'nil)) 'nil))
                  '(:rule-classes (:rewrite :type-prescription))))))
    (name-of-nonempty?
     (and
      nonempty
      (list
       (cons
            'defthm
            (cons (acl2::packn-pos (list name '-of- nonempty)
                                   pkg-witness)
                  (cons (cons name (cons (cons nonempty 'nil) 'nil))
                        'nil)))))))
   (cons
    'encapsulate
    (cons
     'nil
     (cons
      '(logic)
      (cons
       (cons
        'encapsulate
        (cons
         (cons name-sig nonempty-sig?)
         (cons name-def
               (append nonempty-def?
                       (cons booleanp-of-name name-of-nonempty?)))))
       'nil)))))))

Theorem: maybe-pseudo-event-formp-of-defconstrained-recognizer-fn

(defthm maybe-pseudo-event-formp-of-defconstrained-recognizer-fn
  (b* ((event (defconstrained-recognizer-fn name nonempty)))
    (acl2::maybe-pseudo-event-formp event))
  :rule-classes :rewrite)