Raw constructor for honsed fn-info-elt-p structures.
Syntax:
(honsed-fn-info-elt source-fn target-fn iso-thm osi-thm arg-types result-types)
This is identical to fn-info-elt, except that we hons the structure we are creating.
This is an ordinary honsing constructor introduced by std::defaggregate.
Function:
(defun honsed-fn-info-elt (source-fn target-fn iso-thm osi-thm arg-types result-types) (declare (xargs :guard (and (symbolp source-fn) (symbolp-or-lambdap target-fn) (symbolp iso-thm) (symbolp osi-thm) (symbol-listp arg-types) (symbol-listp result-types)))) (mbe :logic (fn-info-elt source-fn target-fn iso-thm osi-thm arg-types result-types) :exec (hons (hons 'source-fn source-fn) (hons (hons 'target-fn target-fn) (hons (hons 'iso-thm iso-thm) (hons (hons 'osi-thm osi-thm) (hons (hons 'arg-types arg-types) (hons (hons 'result-types result-types) nil))))))))