		Search-engine friendly clone of the ACL2 documentation.

Deffixtype-alias

Deffixtype-alias-implementation

Implementation of deffixtype-alias.

Macro: deffixtype-alias

(defmacro deffixtype-alias (alias type &key pred fix equiv)
 (cons
  'make-event
  (cons
   (cons
       'deffixtype-alias-fn
       (cons (cons 'quote (cons alias 'nil))
             (cons (cons 'quote (cons type 'nil))
                   (cons (cons 'quote (cons pred 'nil))
                         (cons (cons 'quote (cons fix 'nil))
                               (cons (cons 'quote (cons equiv 'nil))
                                     '((w state))))))))
   'nil)))

Definitions and Theorems

Function: deffixtype-alias-fn

(defun deffixtype-alias-fn (alias type pred fix equiv wrld)
 (declare (xargs :guard (plist-worldp wrld)))
 (let ((__function__ 'deffixtype-alias-fn))
  (declare (ignorable __function__))
  (b*
   ((table (get-fixtypes-alist wrld))
    (info (find-fixtype type table))
    ((fixtype info) info)
    (pred-events
     (and
      pred
      (cons
       (cons
        'defmacro
        (cons
         pred
         (cons '(x)
               (cons (cons 'list
                           (cons (cons 'quote (cons info.pred 'nil))
                                 '(x)))
                     'nil))))
       (cons (cons 'add-macro-fn
                   (cons pred (cons info.pred 'nil)))
             'nil))))
    (fix-events
     (and
      fix
      (cons
       (cons
        'defmacro
        (cons
          fix
          (cons '(x)
                (cons (cons 'list
                            (cons (cons 'quote (cons info.fix 'nil))
                                  '(x)))
                      'nil))))
       (cons (cons 'add-macro-fn
                   (cons fix (cons info.fix 'nil)))
             'nil))))
    (equiv-events
     (and
      equiv
      (cons
       (cons
        'defmacro
        (cons
         equiv
         (cons
              '(x y)
              (cons (cons 'list
                          (cons (cons 'quote (cons info.equiv 'nil))
                                '(x y)))
                    'nil))))
       'nil)))
    (deffixtype-event
     (cons
      'deffixtype
      (cons
           alias
           (cons ':pred
                 (cons (or pred info.pred)
                       (cons ':fix
                             (cons (or fix info.fix)
                                   (cons ':equiv
                                         (cons (or equiv info.equiv)
                                               'nil))))))))))
   (cons
    'encapsulate
    (cons
        'nil
        (append pred-events
                (append fix-events
                        (append equiv-events
                                (cons deffixtype-event 'nil)))))))))