		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)