• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
    • Std/lists
    • Omaps
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
    • Std/osets
    • Std/io
    • Std/basic
    • Std/system
    • Std/typed-lists
      • Std/typed-lists/character-listp
      • Std/typed-lists/symbol-listp
      • Std/typed-lists/boolean-listp
      • Std/typed-lists/string-listp
      • Std/typed-lists/eqlable-listp
      • Theorems-about-true-list-lists
      • Std/typed-lists/atom-listp
      • Unsigned-byte-listp
        • Defbytelist
          • Defbytelist-standard-instances
          • Defbytelist-implementation
            • Defbytelist-fn
            • Defbytelist-macro-definition
        • Unsigned-byte-list-fix
      • Cons-listp
      • Cons-list-listp
      • Signed-byte-listp
      • String-or-symbol-listp
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Defbytelist-implementation

Defbytelist-macro-definition

Definition of the defbytelist macro.

Macro: defbytelist

(defmacro defbytelist (type &key elt-type
                            pred fix equiv parents short long)
 (cons
  'make-event
  (cons
   (cons
    'defbytelist-fn
    (cons
     (cons 'quote (cons type 'nil))
     (cons
      (cons 'quote (cons elt-type 'nil))
      (cons
       (cons 'quote (cons pred 'nil))
       (cons
            (cons 'quote (cons fix 'nil))
            (cons (cons 'quote (cons equiv 'nil))
                  (cons (cons 'quote (cons parents 'nil))
                        (cons short (cons long '((w state)))))))))))
   'nil)))