		Search-engine friendly clone of the ACL2 documentation.

Crypto-hdwallet

Wallet

Entry point to the ACL2 code of the wallet.

For the main documentation topic, please go up one level to CRYPTO-HDWALLET.

This is a macro, with an associated function as is customary. The function processes the inputs from the shell script and displays the resulting message. The macro wraps the function call in a make-event that keeps the output ``clean'' and that automatically passes the ACL2 state to the function. The macro is called with the strings from the shell script as arguments.

Macro: wallet

(defmacro
 wallet (&rest inputs)
 (cons
  'with-output
  (cons
   ':off
   (cons
    ':all
    (cons
     ':on
     (cons
        'error
        (cons (cons 'make-event
                    (cons (cons 'wallet-fn
                                (cons (cons 'list inputs) '(state)))
                          '(:on-behalf-of :quiet)))
              'nil)))))))

Definitions and Theorems

Function: wallet-fn

(defun wallet-fn (inputs state)
       (declare (xargs :stobjs (state)))
       (declare (xargs :guard (string-listp inputs)))
       (b* (((mv msg state)
             (process-command inputs state))
            (- (cw "~%~@0~%" msg)))
           (value '(value-triple :invisible))))