		Search-engine friendly clone of the ACL2 documentation.

Warnings

Ok

A convenient shorthand for calling vl-warninglist-fix.

(ok) is just syntactic sugar for:

(vl-warninglist-fix warnings)

This is often useful as a base case in functions that sometimes create warnings. The name of the warnings accumulator to fix can also be specified, e.g.,:

(ok acc) == (vl-warninglist-fix acc)

Macro: ok

(defmacro ok (&optional (warnings 'warnings))
          (cons 'vl-warninglist-fix
                (cons warnings 'nil)))

Definitions and Theorems

Theorem: ok-correct

(defthm ok-correct
        (and (equal (ok x) (vl-warninglist-fix x))
             (equal (ok)
                    (vl-warninglist-fix warnings)))
        :rule-classes nil)