		Search-engine friendly clone of the ACL2 documentation.

Aig-constructors

Aig-implies

(aig-implies x y) constructs an AIG representing (implies x y).

We try to lazily avoid evaluating y.

Macro: aig-implies

(defmacro aig-implies (x y)
 (cons
  'mbe
  (cons
   ':logic
   (cons
    (cons 'aig-implies-fn
          (cons x (cons y 'nil)))
    (cons
     ':exec
     (cons
      (cons
       'let
       (cons
        (cons (cons 'aig-implies-x-do-not-use-elsewhere
                    (cons x 'nil))
              'nil)
        (cons
         (cons
          'if
          (cons
           '(eq nil aig-implies-x-do-not-use-elsewhere)
           (cons
            't
            (cons
             (cons
              'aig-implies-fn
              (cons
               'aig-implies-x-do-not-use-elsewhere
               (cons
                   (cons 'check-vars-not-free
                         (cons '(aig-implies-x-do-not-use-elsewhere)
                               (cons y 'nil)))
                   'nil)))
             'nil))))
         'nil)))
      'nil))))))

Subtopics

Aig-implies-fn