		Search-engine friendly clone of the ACL2 documentation.

Deflist-of-len-implementation

Deflist-of-len-macro-definition

Definition of the deflist-of-len macro.

Macro: deflist-of-len

(defmacro deflist-of-len (type &key list-type length
                               pred fix equiv parents short long)
 (cons
  'make-event
  (cons
   (cons
    'deflist-of-len-fn
    (cons
     (cons 'quote (cons type 'nil))
     (cons
      (cons 'quote (cons list-type 'nil))
      (cons
       (cons 'quote (cons length '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)))