• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
    • Std/alists
    • Obags
    • Std/util
      • Defprojection
      • Deflist
      • Defaggregate
      • Define
      • Defmapping
      • Defenum
      • Add-io-pairs
      • Defalist
      • Defmapappend
      • Returns-specifiers
      • Defarbrec
      • Define-sk
      • Defines
      • Error-value-tuples
      • Defmax-nat
      • Defmin-int
      • Deftutorial
      • Extended-formals
      • Defrule
      • Defval
      • Defsurj
      • Defiso
      • Defconstrained-recognizer
      • Deffixer
        • Deffixer-implementation
        • Defconstrained-recognizer-implementation
          • Defconstrained-recognizer-fn
          • Defconstrained-recognizer-definition
      • Defmvtypes
      • Defconsts
      • Support
      • Defthm-signed-byte-p
      • Defthm-unsigned-byte-p
      • Defthm-natp
      • Defund-sk
      • Defmacro+
      • Defsum
      • Defthm-commutative
      • Definj
      • Defirrelevant
      • Defredundant
    • Std/strings
    • Std/io
    • Std/osets
    • Std/basic
    • Std/system
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• 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)