		Search-engine friendly clone of the ACL2 documentation.

Cond

Conditional based on if-then-else

Cond is the construct for IF, THEN, ELSE IF, ... The test is against nil. The argument list for cond is a list of ``cond clauses'', each of which is a list. In ACL2, cond clauses must have length 1 or 2.

; Example 1.  The form
  (COND ((CONSP X) (FOO X Y))
        ((SYMBOLP X) (BAR X Y))
        (T (LIST X Y)))
; abbreviates the following.
  (IF (CONSP X)
      (FOO X Y)
      (IF (SYMBOLP X)
          (BAR X Y)
          (LIST X Y)))

; Example 2.  The form
  (COND ((CONSP X))
        ((SYMBOLP X) (BAR X Y)))
; abbreviates the following.
  (OR (CONSP X)
      (IF (SYMBOLP X) (BAR X Y) NIL))

The results above were obtained by typing :trans1 followed by the form in the ACL2 loop, and then hitting <RETURN>. See trans1. You can experiment in this way to see other such examples.

Cond is a Common Lisp macro. See any Common Lisp documentation for more information.

Macro: cond

(defmacro cond (&rest clauses)
  (declare (xargs :guard (cond-clausesp clauses)))
  (cond-macro clauses))

Function: cond-macro

(defun cond-macro (clauses)
  (declare (xargs :guard (cond-clausesp clauses)))
  (if (consp clauses)
      (if (and (eq (car (car clauses)) t)
               (eq (cdr clauses) nil))
          (if (cdr (car clauses))
              (car (cdr (car clauses)))
            (car (car clauses)))
        (if (cdr (car clauses))
            (list 'if
                  (car (car clauses))
                  (car (cdr (car clauses)))
                  (cond-macro (cdr clauses)))
          (list 'or
                (car (car clauses))
                (cond-macro (cdr clauses)))))
    nil))