		Search-engine friendly clone of the ACL2 documentation.
Errors
Defresult-fn

Signature
(defresult-fn type desc name enable wrld) → event
Arguments: wrld — Guard (plist-worldp wrld).
Definitions and Theorems

Function: defresult-fn
(defun defresult-fn (type desc name enable wrld)
 (declare (xargs :guard (plist-worldp wrld)))
 (let ((__function__ 'defresult-fn))
  (declare (ignorable __function__))
  (b* ((fty-table (fty::get-fixtypes-alist wrld))
       (fty-info (fty::find-fixtype type fty-table))
       (typep (fty::fixtype->pred fty-info))
       (name (or name type))
       (name-result (add-suffix name "-RESULT"))
       (name-resultp (add-suffix name "-RESULTP"))
       (short (str::cat "Fixtype of " desc " and errors."))
       (typep-when-name-resultp-and-not-errorp
            (packn-pos (list typep '-when-
                             name-resultp '-and-not-errorp)
                       name)))
   (cons
    'encapsulate
    (cons
     'nil
     (cons
      (cons
       'fty::defflatsum
       (cons
        name-result
        (cons
         ':short
         (cons
          short
          (cons
           (cons ':ok (cons type 'nil))
           (cons
            '(:err error)
            (cons
             ':pred
             (cons
              name-resultp
              (and
               enable
               (cons
                ':prepwork
                (cons
                 (cons
                  (cons
                   'defrulel
                   (cons
                    'disjoint
                    (cons
                     (cons
                      'implies
                      (cons
                          '(errorp x)
                          (cons (cons 'not
                                      (cons (cons typep '(x)) 'nil))
                                'nil)))
                     (cons ':enable (cons enable 'nil)))))
                  'nil)
                 'nil)))))))))))
      (cons
       (cons
        'defruled
        (cons typep-when-name-resultp-and-not-errorp
              (cons (cons 'implies
                          (cons (cons 'and
                                      (cons (cons name-resultp '(x))
                                            '((not (errorp x)))))
                                (cons (cons typep '(x)) 'nil)))
                    (cons ':enable
                          (cons name-resultp 'nil)))))
       'nil)))))))