		Search-engine friendly clone of the ACL2 documentation.

Propiso-info-p

Honsed-propiso-info

Raw constructor for honsed propiso-info-p structures.

Syntax:

(honsed-propiso-info iso-osi-ruleset-name iso-ruleset-name 
                     osi-ruleset-name hints-map world)

This is identical to propiso-info, except that we hons the structure we are creating.

Definition

This is an ordinary honsing constructor introduced by std::defaggregate.

Function: honsed-propiso-info

(defun honsed-propiso-info
       (iso-osi-ruleset-name iso-ruleset-name
                             osi-ruleset-name hints-map world)
 (declare (xargs :guard (and (symbolp iso-osi-ruleset-name)
                             (symbolp iso-ruleset-name)
                             (symbolp osi-ruleset-name)
                             (symbol-alistp hints-map)
                             (plist-worldp world))))
 (mbe
  :logic (propiso-info iso-osi-ruleset-name iso-ruleset-name
                       osi-ruleset-name hints-map world)
  :exec (hons (hons 'iso-osi-ruleset-name
                    iso-osi-ruleset-name)
              (hons (hons 'iso-ruleset-name
                          iso-ruleset-name)
                    (hons (hons 'osi-ruleset-name
                                osi-ruleset-name)
                          (hons (hons 'hints-map hints-map)
                                (hons (hons 'world world) nil)))))))