		Search-engine friendly clone of the ACL2 documentation.

Definterface-encrypt-init

Definterface-encrypt-init-macro-definition

Definition of the definterface-encrypt-init macro.

Macro: definterface-encrypt-init

(defmacro definterface-encrypt-init
          (name &key key-size init-size
                name-encrypt-bits name-decrypt-bits
                name-encrypt-bytes name-decrypt-bytes
                topic parents short long)
 (cons
  'make-event
  (cons
   (cons
    'definterface-encrypt-init-fn
    (cons
     (cons 'quote (cons name 'nil))
     (cons
      key-size
      (cons
       init-size
       (cons
        (cons 'quote
              (cons name-encrypt-bits 'nil))
        (cons
         (cons 'quote
               (cons name-decrypt-bits 'nil))
         (cons
           (cons 'quote
                 (cons name-encrypt-bytes 'nil))
           (cons (cons 'quote
                       (cons name-decrypt-bytes 'nil))
                 (cons (cons 'quote (cons topic 'nil))
                       (cons (cons 'quote (cons parents 'nil))
                             (cons short (cons long 'nil))))))))))))
   'nil)))