		Search-engine friendly clone of the ACL2 documentation.

Process-smtlink-hints

Set-wrld-len

Set :wrld-fn-len

Signature
(set-wrld-len content hint) → new-hint
Arguments: content — Guard (natp content).; hint — Guard (smtlink-hint-p hint).
Returns: new-hint — Type (smtlink-hint-p new-hint).

Definitions and Theorems

Function: set-wrld-len

(defun set-wrld-len (content hint)
  (declare (xargs :guard (and (natp content)
                              (smtlink-hint-p hint))))
  (let ((acl2::__function__ 'set-wrld-len))
    (declare (ignorable acl2::__function__))
    (b* ((hint (smtlink-hint-fix hint))
         (new-hint (change-smtlink-hint hint
                                        :wrld-fn-len content)))
      new-hint)))

Theorem: smtlink-hint-p-of-set-wrld-len

(defthm smtlink-hint-p-of-set-wrld-len
  (b* ((new-hint (set-wrld-len content hint)))
    (smtlink-hint-p new-hint))
  :rule-classes :rewrite)