		Search-engine friendly clone of the ACL2 documentation.

Defbyte-implementation

Defbyte-check-size

Check if the size input is valid.

Signature
(defbyte-check-size size wrld) → (mv valid value)
Arguments: wrld — Guard (plist-worldp wrld).
Returns: valid — A booleanp.; value — A ACL2::maybe-posp.

The first result is t if the input is valid, otherwise it is nil. If the input is a call of a unary function, we do not check here that it is guard-verified and that it provably denotes a positive integer. In these cases, the call to the macro will fail (hopefully in a comprehensible way).

If the input is valid and is not a call of a unary function, the second result is the value of the input, which is known in this case. Otherwise, the second result is nil.

Definitions and Theorems

Function: defbyte-check-size

(defun defbyte-check-size (size wrld)
  (declare (xargs :guard (plist-worldp wrld)))
  (let ((__function__ 'defbyte-check-size))
    (declare (ignorable __function__))
    (b* (((when (posp size)) (mv t size))
         (const? (acl2::defined-constant size wrld))
         ((when const?)
          (b* ((value (unquote const?)))
            (if (posp value)
                (mv t value)
              (mv nil nil))))
         ((unless (acl2::tuplep 1 size))
          (mv nil nil))
         (fn (car size)))
      (if (and (function-symbolp fn wrld)
               (= 0 (arity fn wrld)))
          (mv t nil)
        (mv nil nil)))))