		Search-engine friendly clone of the ACL2 documentation.

Defconstrained-recognizer-implementation

Defconstrained-recognizer-definition

Definition of the defconstrained-recognizer macro.

Macro: defconstrained-recognizer

(defmacro defconstrained-recognizer (name &key nonempty)
  (cons 'make-event
        (cons (cons 'defconstrained-recognizer-fn
                    (cons (cons 'quote (cons name 'nil))
                          (cons (cons 'quote (cons nonempty 'nil))
                                'nil)))
              'nil)))