		Search-engine friendly clone of the ACL2 documentation.

Fgl-object

Fgl-make-isomorphic

FGL binder function whose implementation will try to modify the symbolic representation of the two inputs so that they have Boolean function objects in all the same places. The successp flag (expected to be the binder input's free variable) indicates whether this succeeded.

Signature
(fgl-make-isomorphic successp x y) → (mv * * *)

Definitions and Theorems

Function: fgl-make-isomorphic

(defun fgl-make-isomorphic (successp x y)
  (declare (xargs :guard t))
  (let ((__function__ 'fgl-make-isomorphic))
    (declare (ignorable __function__))
    (mv (ec-call (car successp)) x y)))