		Search-engine friendly clone of the ACL2 documentation.

Rlp-error-non-optimal-short-length

Make-rlp-error-non-optimal-short-length

Basic constructor macro for rlp-error-non-optimal-short-length structures.

Syntax

(make-rlp-error-non-optimal-short-length [:fragment <fragment>])

This is the usual way to construct rlp-error-non-optimal-short-length structures. It simply conses together a structure with the specified fields.

This macro generates a new rlp-error-non-optimal-short-length structure from scratch. See also change-rlp-error-non-optimal-short-length, which can "change" an existing structure, instead.

Definition

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

Macro: make-rlp-error-non-optimal-short-length

(defmacro make-rlp-error-non-optimal-short-length (&rest args)
  (std::make-aggregate 'rlp-error-non-optimal-short-length
                       args '((:fragment))
                       'make-rlp-error-non-optimal-short-length
                       nil))

Function: rlp-error-non-optimal-short-length

(defun rlp-error-non-optimal-short-length (fragment)
  (declare (xargs :guard (byte-listp fragment)))
  (declare (xargs :guard t))
  (let ((__function__ 'rlp-error-non-optimal-short-length))
    (declare (ignorable __function__))
    (b* ((fragment (mbe :logic (byte-list-fix fragment)
                        :exec fragment)))
      (cons :non-optimal-short-length (list fragment)))))