		Search-engine friendly clone of the ACL2 documentation.
Constants-conversions-and-bounds
Np-def-n

Signature
(np-def-n n) → *
Definitions and Theorems

Function: np-def-n
(defun np-def-n (n)
 (declare (xargs :guard (posp n)))
 (let ((__function__ 'np-def-n))
  (declare (ignorable __function__))
  (let* ((str-n (symbol-name (if (< n 10)
                                 (acl2::packn (list 0 n))
                               (acl2::packn (list n)))))
         (digits (symbol-name (acl2::packn (list n))))
         (2^xy (mk-name "*2^" digits "*"))
         (nxyp (mk-name "N" str-n "P"))
         (nxy (mk-name "N" str-n))
         (ixyp (mk-name "I" str-n "P"))
         (ixy (mk-name "I" str-n))
         (ntoi (mk-name "N" str-n "-TO-I" str-n))
         (iton (mk-name "I" str-n "-TO-N" str-n)))
   (list
    (cons 'defconst
          (cons 2^xy
                (cons (cons 'expt (cons '2 (cons n 'nil)))
                      'nil)))
    (cons
     'define
     (cons
      nxyp
      (cons
       '(x)
       (cons
        ':inline
        (cons
         't
         (cons
          ':no-function
          (cons
           't
           (cons
            ':enabled
            (cons
             't
             (cons ':parents
                   (cons '(constants-conversions-and-bounds)
                         (cons (cons 'unsigned-byte-p (cons n '(x)))
                               'nil))))))))))))
    (cons
     'define
     (cons
      nxy
      (cons
       '((x integerp))
       (cons
        ':inline
        (cons
         't
         (cons
          ':no-function
          (cons
           't
           (cons
            ':enabled
            (cons
             't
             (cons
              ':parents
              (cons
               '(constants-conversions-and-bounds)
               (cons
                (cons
                 'mbe
                 (cons
                  ':logic
                  (cons
                      (cons 'loghead (cons n '(x)))
                      (cons ':exec
                            (cons (cons 'logand
                                        (cons (1- (expt 2 n)) '(x)))
                                  'nil)))))
                'nil))))))))))))
    (cons
     'define
     (cons
      ixyp
      (cons
       '(x)
       (cons
        ':inline
        (cons
         't
         (cons
          ':no-function
          (cons
           't
           (cons
            ':enabled
            (cons
               't
               (cons ':parents
                     (cons '(constants-conversions-and-bounds)
                           (cons (cons 'signed-byte-p (cons n '(x)))
                                 'nil))))))))))))
    (cons
     'define
     (cons
      ixy
      (cons
       '((x integerp))
       (cons
        ':inline
        (cons
         't
         (cons
          ':no-function
          (cons
           't
           (cons
            ':enabled
            (cons
             't
             (cons
              ':parents
              (cons
               '(constants-conversions-and-bounds)
               (cons
                (cons
                 'mbe
                 (cons
                  ':logic
                  (cons
                       (cons 'logext (cons n '(x)))
                       (cons ':exec
                             (cons (cons 'fast-logext (cons n '(x)))
                                   'nil)))))
                'nil))))))))))))
    (cons
     'define
     (cons
      ntoi
      (cons
       (cons
         (cons 'x
               (cons nxyp
                     (cons ':type
                           (cons (cons 'unsigned-byte (cons n 'nil))
                                 'nil))))
         'nil)
       (cons
        ':inline
        (cons
         't
         (cons
          ':no-function
          (cons
           't
           (cons
            ':enabled
            (cons
             't
             (cons
              ':parents
              (cons
               '(constants-conversions-and-bounds)
               (cons
                ':guard-hints
                (cons
                 '(("Goal"
                    :in-theory
                    (enable
                     logext-when-unsigned-byte-p-and-sign-changes)))
                 (cons
                  (cons
                   'mbe
                   (cons
                    ':logic
                    (cons
                     (cons 'logext (cons n '(x)))
                     (cons
                      ':exec
                      (cons
                       (cons
                        'if
                        (cons
                         (cons
                              '<
                              (cons 'x (cons (expt 2 (1- n)) 'nil)))
                         (cons
                          'x
                          (cons
                             (cons '-
                                   (cons 'x (cons (expt 2 n) 'nil)))
                             'nil))))
                       'nil)))))
                  'nil))))))))))))))
    (cons
     'define
     (cons
      iton
      (cons
       (cons
           (cons 'x
                 (cons ixyp
                       (cons ':type
                             (cons (cons 'signed-byte (cons n 'nil))
                                   'nil))))
           'nil)
       (cons
        ':inline
        (cons
         't
         (cons
          ':no-function
          (cons
           't
           (cons
            ':enabled
            (cons
             't
             (cons
              ':parents
              (cons
               '(constants-conversions-and-bounds)
               (cons
                ':guard-hints
                (cons
                 '(("Goal"
                    :in-theory
                    (enable
                      loghead-when-signed-byte-p-and-sign-changes)))
                 (cons
                  (cons
                   'mbe
                   (cons
                    ':logic
                    (cons
                     (cons 'loghead (cons n '(x)))
                     (cons
                      ':exec
                      (cons
                       (cons
                        'if
                        (cons
                         '(>= x 0)
                         (cons
                          'x
                          (cons
                             (cons '+
                                   (cons 'x (cons (expt 2 n) 'nil)))
                             'nil))))
                       'nil)))))
                  'nil))))))))))))))
    (cons 'add-to-ruleset
          (cons 'nwp-defs
                (cons (cons 'quote
                            (cons (cons nxyp 'nil) 'nil))
                      'nil)))
    (cons 'add-to-ruleset
          (cons 'nw-defs
                (cons (cons 'quote
                            (cons (cons nxy 'nil) 'nil))
                      'nil)))
    (cons 'add-to-ruleset
          (cons 'iwp-defs
                (cons (cons 'quote
                            (cons (cons ixyp 'nil) 'nil))
                      'nil)))
    (cons 'add-to-ruleset
          (cons 'iw-defs
                (cons (cons 'quote
                            (cons (cons ixy 'nil) 'nil))
                      'nil)))
    (cons 'add-to-ruleset
          (cons 'nw-to-iw-defs
                (cons (cons 'quote
                            (cons (cons ntoi 'nil) 'nil))
                      'nil)))
    (cons 'add-to-ruleset
          (cons 'iw-to-nw-defs
                (cons (cons 'quote
                            (cons (cons iton 'nil) 'nil))
                      'nil)))))))