		Search-engine friendly clone of the ACL2 documentation.

Defdigit-grouping-implementation

Defdigit-grouping-macro-definition

Definition of the defdigit-grouping macro.

Macro: defdigit-grouping

(defmacro defdigit-grouping
          (name &key smaller larger group-bendian
                group-lendian ungroup-bendian
                ungroup-lendian parents short long)
 (cons
  'make-event
  (cons
   (cons
    'defdigit-grouping-fn
    (cons
     (cons 'quote (cons name 'nil))
     (cons
      (cons 'quote (cons smaller 'nil))
      (cons
       (cons 'quote (cons larger 'nil))
       (cons
        (cons 'quote (cons group-bendian 'nil))
        (cons
         (cons 'quote (cons group-lendian 'nil))
         (cons
              (cons 'quote
                    (cons ungroup-bendian 'nil))
              (cons (cons 'quote
                          (cons ungroup-lendian 'nil))
                    (cons (cons 'quote (cons parents 'nil))
                          (cons (cons 'quote (cons short 'nil))
                                (cons (cons 'quote (cons long 'nil))
                                      '((w state)))))))))))))
   'nil)))