title: The symbol PUT (in package "ACL2") has neither a function nor macro definition in ACL2
body: <p>All</p>
  <p>I just begin my self-teach tour of ACL2, and I try to test some example of <a href="https://www.cs.utexas.edu/users/moore/acl2/v8-5/combined-manual/index.html?topic=ACL2____INTRODUCTION-TO-REWRITE-RULES-PART-1" rel="nofollow noreferrer">Introduction-to-rewrite-rules-part-1</a>.</p>
  <p>Here is my code,</p>
  <pre class="lang-lisp prettyprint-override"><code>(implies (and (natp i)
                (&lt; i (len a)))
           (equal (put i v (append a b))
                  (append (put i v a) b)))
  
  (put i v (append a b))
  </code></pre>
  <p>And I got this error</p>
  <blockquote>
  <p>ACL2 Error in TOP-LEVEL:  The symbol PUT (in package &quot;ACL2&quot;) has neither
  a function nor macro definition in ACL2.  Please define it; or perhaps
  you meant ACL2-PC::PUT, which has the same name but is in a different
  package.  See :DOC near-misses.  Note:  this error occurred in the
  context (PUT I V (APPEND A B)).</p>
  </blockquote>
  <p>It seem I miss the <code>defun</code> of <code>put</code>, I try to google the define of put in ACL2 packages, but without luck.
  Any idea I can get this example work?</p>
  <p>Thanks</p>