		Search-engine friendly clone of the ACL2 documentation.

Bip32-ext-key-pub

Make-bip32-ext-key-pub

Basic constructor macro for bip32-ext-key-pub structures.

Syntax

(make-bip32-ext-key-pub [:get <get>])

This is the usual way to construct bip32-ext-key-pub structures. It simply conses together a structure with the specified fields.

This macro generates a new bip32-ext-key-pub structure from scratch. See also change-bip32-ext-key-pub, which can "change" an existing structure, instead.

Definition

This is an ordinary make- macro introduced by fty::defprod.

Macro: make-bip32-ext-key-pub

(defmacro make-bip32-ext-key-pub (&rest args)
  (std::make-aggregate 'bip32-ext-key-pub
                       args '((:get))
                       'make-bip32-ext-key-pub
                       nil))

Function: bip32-ext-key-pub

(defun bip32-ext-key-pub (get)
  (declare (xargs :guard (bip32-ext-pub-key-p get)))
  (declare (xargs :guard t))
  (let ((__function__ 'bip32-ext-key-pub))
    (declare (ignorable __function__))
    (b* ((get (mbe :logic (bip32-ext-pub-key-fix get)
                   :exec get)))
      (cons :pub (list get)))))