		Search-engine friendly clone of the ACL2 documentation.

Std/system/function-queries

Guard-theorem-no-simplify

A version of guard-theorem that does no simplification.

This definition is based on the definition of ACL2 source function guard-theorem, with the simplify argument set to nil, with no state argument, and with new safe-mode and gc-off arguments; the latter two can reasonably be (f-get-global 'safe-mode state) and (gc-off state), respectively.

An advantage of not having the state argument is that this function can be called via magic-ev-fncall.

Definitions and Theorems

Function: guard-theorem-no-simplify

(defun guard-theorem-no-simplify
       (fn guard-debug wrld safe-mode gc-off)
 (cond
  ((not (getpropc fn 'unnormalized-body
                  nil wrld))
   *t*)
  (t
   (let ((names (or (getpropc fn 'recursivep nil wrld)
                    (list fn))))
     (mv-let
        (cl-set ttree)
        (guard-clauses-for-clique names guard-debug :do-not-simplify
                                  wrld safe-mode gc-off nil)
       (declare (ignore ttree))
       (termify-clause-set cl-set))))))