		Search-engine friendly clone of the ACL2 documentation.

Fgl-rewrite-rules

Collect-cmr-rewrites-for-formula-name

Signature
(collect-cmr-rewrites-for-formula-name name world) → rewrites
Arguments: name — Guard (symbolp name).; world — Guard (plist-worldp world).
Returns: rewrites — Type (cmr::rewritelist-p rewrites).

Definitions and Theorems

Function: collect-cmr-rewrites-for-formula-name

(defun
 collect-cmr-rewrites-for-formula-name
 (name world)
 (declare (xargs :guard (and (symbolp name)
                             (plist-worldp world))))
 (let
  ((__function__ 'collect-cmr-rewrites-for-formula-name))
  (declare (ignorable __function__))
  (b*
   ((form (acl2::meta-extract-formula-w name world))
    ((mv err rewrites)
     (cmr::parse-rewrites-from-term form world))
    ((when (and err (not rewrites)))
     (er hard?
         'collect-cmr-rewrites-for-formula-name
         "No rewrites parsed from ~x0: ~@1"
         name err)))
   (and
    err
    (cw
     "Warning: incomplete conversion from formula to rewrites for ~x0: ~@1~%"
     name err))
   rewrites)))

Theorem: rewritelist-p-of-collect-cmr-rewrites-for-formula-name

(defthm
 rewritelist-p-of-collect-cmr-rewrites-for-formula-name
 (b* ((rewrites (collect-cmr-rewrites-for-formula-name name world)))
     (cmr::rewritelist-p rewrites))
 :rule-classes :rewrite)