CASE

conditional based on if-then-else using eql 
Major Section:  ACL2-BUILT-INS


Example Form:
(case typ
  ((:character foo)
   (open file-name :direction :output))
  (bar (open-for-bar file-name))
  (otherwise
   (my-error "Illegal.")))
is the same as 
(cond ((member typ '(:character foo))
       (open file-name :direction :output))
      ((eql typ 'bar)
       (open-for-bar file-name))
      (t (my-error "Illegal.")))
which in turn is the same as 
(if (member typ '(:character foo))
    (open file-name :direction :output)
    (if (eql typ 'bar)
        (open-for-bar file-name)
        (my-error "Illegal.")))
Notice the quotations that appear in the example above: '(:character foo) and 'bar.

General Forms:
(case expr
  (x1 val-1)
  ...
  (xk val-k)
  (otherwise val-k+1))

(case expr
  (x1 val-1)
  ...
  (xk val-k)
  (t val-k+1))

(case expr
  (x1 val-1)
  ...
  (xk val-k))
where each xi is either eqlablep or a true list of eqlablep objects. The final otherwise or t case is optional.

Case is defined in Common Lisp. See any Common Lisp documentation for more information.