		Search-engine friendly clone of the ACL2 documentation.
Defdigits-implementation
Defdigits-macro-definition

Definition of the defdigits macro.
Macro: defdigits
(defmacro defdigits (name &key base digit-pred digit-fix
                          digits-pred digits-fix bendian-to-nat
                          lendian-to-nat nat-to-bendian
                          nat-to-lendian digit-pred-hints
                          digit-fix-hints digit-pred-guard-hints
                          digit-fix-guard-hints digits-pred-hints
                          digits-fix-hints digits-pred-guard-hints
                          digits-fix-guard-hints
                          digits-description parents short long)
 (cons
  'make-event
  (cons
   (cons
    'defdigits-fn
    (cons
     (cons 'quote (cons name 'nil))
     (cons
      (cons 'quote (cons base 'nil))
      (cons
       (cons 'quote (cons digit-pred 'nil))
       (cons
        (cons 'quote (cons digit-fix 'nil))
        (cons
         (cons 'quote (cons digits-pred 'nil))
         (cons
          (cons 'quote (cons digits-fix 'nil))
          (cons
           (cons 'quote (cons bendian-to-nat 'nil))
           (cons
            (cons 'quote (cons lendian-to-nat 'nil))
            (cons
             (cons 'quote (cons nat-to-bendian 'nil))
             (cons
              (cons 'quote (cons nat-to-lendian 'nil))
              (cons
               (cons 'quote
                     (cons digit-pred-hints 'nil))
               (cons
                (cons 'quote
                      (cons digit-fix-hints 'nil))
                (cons
                 (cons 'quote
                       (cons digit-pred-guard-hints 'nil))
                 (cons
                  (cons 'quote
                        (cons digit-fix-guard-hints 'nil))
                  (cons
                   (cons 'quote
                         (cons digits-pred-hints 'nil))
                   (cons
                    (cons 'quote
                          (cons digits-fix-hints 'nil))
                    (cons
                     (cons 'quote
                           (cons digits-pred-guard-hints 'nil))
                     (cons
                      (cons 'quote
                            (cons digits-fix-guard-hints 'nil))
                      (cons
                       (cons 'quote
                             (cons digits-description 'nil))
                       (cons
                        (cons 'quote (cons parents 'nil))
                        (cons
                           (cons 'quote (cons short 'nil))
                           (cons (cons 'quote (cons long 'nil))
                                 '((w state)))))))))))))))))))))))))
   'nil)))