		Search-engine friendly clone of the ACL2 documentation.

Defbytelist-standard-instances

Defsbytelist

Specialized form of defbytelist for generating standard fixtypes of true lists of signed bytes of explicit integer sizes.

This macro just takes a positive integer as input.

This macro generates fixtypes called acl2::sbyte<size>-list, where <size> consists of the decimal digits of the size. The recognizer, fixer, and equivalence are called acl2::sbyte<size>-listp, acl2::sbyte<size>-list-fix, and acl2::sbyte<size>-list-equiv.

This also generates some standardized XDOC parents and short, and no XDOC long.

Macro: defsbytelist

(defmacro defsbytelist (size)
 (declare (xargs :guard (posp size)))
 (cons
  'defbytelist
  (cons
   (acl2::packn (list 'acl2::sbyte size '-list))
   (cons
    ':elt-type
    (cons
     (acl2::packn (list 'acl2::sbyte size))
     (cons
      ':pred
      (cons
       (acl2::packn (list 'acl2::sbyte size '-listp))
       (cons
        ':fix
        (cons
         (acl2::packn (list 'acl2::sbyte size '-list-fix))
         (cons
          ':equiv
          (cons
           (acl2::packn (list 'acl2::sbyte size '-list-equiv))
           (cons
            ':parents
            (cons
             '(defbytelist-standard-instances)
             (cons
              ':short
              (cons
               (concatenate
                   'string
                   "Fixtype of true lists of signed bytes of size "
                   (coerce (explode-nonnegative-integer size 10 nil)
                           'string)
                   ".")
               'nil)))))))))))))))