Defchoose2-implementation
Implementation of defchoose2.
Macro: defchoose2
(defmacro defchoose2 (sofun &rest rest)
(list 'progn
(list* 'defchoose sofun rest)
(list 'defsoft sofun))) Macro: defchoose2
(defmacro acl2::defchoose2 (&rest args)
(list* 'defchoose2 args))
