		Search-engine friendly clone of the ACL2 documentation.

Utilities

Debuggable-and

Alternative to and that prints a message where it fails.

(debuggable-and ...) is the same as (and ...), but prints a message when any of the conjuncts fails. For instance,

VL !>(debuggable-and (natp 3)
                     (symbolp 'foo)
                     (consp 4)
                     (symbolp 'bar))
Debuggable-and failure: (CONSP 4).
NIL
VL !>

This can be useful when writing unit tests, checking guards, etc.

Definitions and Theorems

Function: debuggable-and-fn

(defun debuggable-and-fn (args)
 (cond
  ((atom args) t)
  (t
   (cons
    'and
    (cons
     (cons
      'or
      (cons
        (car args)
        (cons (cons 'cw
                    (cons '"Debuggable-and failure: ~x0.~%"
                          (cons (cons 'quote (cons (car args) 'nil))
                                'nil)))
              'nil)))
     (cons (debuggable-and-fn (cdr args))
           'nil))))))