		Search-engine friendly clone of the ACL2 documentation.
Defunit-implementation
Defunit-fn

Event generated by defunit.
Signature
(defunit-fn type value pred fix equiv parents short long) → event
Returns: event — A ACL2::pseudo-event-formp.
Definitions and Theorems

Function: defunit-fn
(defun defunit-fn (type value pred fix equiv parents short long)
 (declare (xargs :guard t))
 (let ((__function__ 'defunit-fn))
  (declare (ignorable __function__))
  (b*
   (((unless (symbolp type))
     (raise
      "The TYPE input must be a symbol, ~
                but it is ~x0 instead."
      type))
    ((unless (keywordp value))
     (raise
      "The VALUE input must be a keyword, ~
                but it is ~x0 instead."
      value))
    ((unless (symbolp pred))
     (raise
      "The :PRED input must be a symbol, ~
                but it is ~x0 instead."
      pred))
    ((unless (symbolp fix))
     (raise
      "The :FIX input must be a symbol, ~
                but it is ~x0 instead."
      fix))
    ((unless (symbolp equiv))
     (raise
      "The :EQUIV input must be a symbol, ~
                but it is ~x0 instead."
      equiv))
    (x (intern-in-package-of-symbol "X" type))
    (pred (or pred (add-suffix-to-fn type "-P")))
    (fix (or fix (add-suffix-to-fn type "-FIX")))
    (equiv (or equiv (add-suffix-to-fn type "-EQUIV")))
    (type-ref
      (concatenate
           'string
           "@(tsee "
           (common-lisp::string-downcase (symbol-package-name type))
           "::"
           (common-lisp::string-downcase (symbol-name type))
           ")"))
    (pred-event
     (cons
      'define
      (cons
       pred
       (cons
        (cons x 'nil)
        (cons
         ':returns
         (cons
          '(yes/no booleanp)
          (cons
           ':parents
           (cons
            (cons type 'nil)
            (cons ':short
                  (cons (concatenate 'string
                                     "Recognizer for " type-ref ".")
                        (cons (cons 'eq (cons x (cons value 'nil)))
                              '(:no-function t))))))))))))
    (fix-event
     (cons
      'std::deffixer
      (cons
       fix
       (cons
        ':pred
        (cons
         pred
         (cons
          ':param
          (cons
           x
           (cons
            ':body-fix
            (cons
             value
             (cons
              ':parents
              (cons
                 (cons type 'nil)
                 (cons ':short
                       (cons (concatenate 'string
                                          "Fixer for " type-ref ".")
                             'nil)))))))))))))
    (type-event
     (cons
      'defsection
      (cons
       type
       (append
        (and parents (list :parents parents))
        (append
         (and short (list :short short))
         (append
          (and long (list :long long))
          (cons
           (cons
            'deffixtype
            (cons
             type
             (cons
              ':pred
              (cons
               pred
               (cons
                ':fix
                (cons
                   fix
                   (cons ':equiv
                         (cons equiv '(:define t :forward t)))))))))
           'nil))))))))
   (cons
    'encapsulate
    (cons 'nil
          (cons '(logic)
                (cons pred-event
                      (cons fix-event (cons type-event 'nil)))))))))