		Search-engine friendly clone of the ACL2 documentation.

Octal

Revappend-nat-to-oct-chars

More efficient version of (revappend (nat-to-oct-chars n) acc).

Signature
(revappend-nat-to-oct-chars n acc) → new-acc
Arguments: n — Guard (natp n).

This strange operation can be useful when building strings by consing together characters in reverse order.

Definitions and Theorems

Function: revappend-nat-to-oct-chars$inline

(defun revappend-nat-to-oct-chars$inline (n acc)
  (declare (xargs :guard (natp n)))
  (let ((acl2::__function__ 'revappend-nat-to-oct-chars))
    (declare (ignorable acl2::__function__))
    (mbe :logic
         (revappend (nat-to-oct-chars n) acc)
         :exec
         (if (zp n)
             (cons #\0 acc)
           (revappend-nat-to-oct-chars-aux n acc)))))

Subtopics

Revappend-nat-to-oct-chars-aux