		Search-engine friendly clone of the ACL2 documentation.

Translate-cmp-smtlink

Wrld-fn-len

Signature
(wrld-fn-len state) → *

Definitions and Theorems

Function: wrld-fn-len

(defun wrld-fn-len (state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'wrld-fn-len))
    (declare (ignorable acl2::__function__))
    (b* ((world (w state)))
      (len (remove-duplicates-eq
                (strip-cadrs (universal-theory :here)))))))