		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)