		Search-engine friendly clone of the ACL2 documentation.

Sd-problem-p

Honsed-sd-problem

Raw constructor for honsed sd-problem-p structures.

Syntax:

(honsed-sd-problem type priority groupsize key ctx)

This is identical to sd-problem, except that we hons the structure we are creating.

Definition

This is an ordinary honsing constructor introduced by defaggregate.

Function: honsed-sd-problem

(defun honsed-sd-problem (type priority groupsize key ctx)
 (declare (xargs :guard (and (symbolp type)
                             (natp priority)
                             (natp groupsize)
                             (sd-key-p key)
                             (vl-context1-p ctx))))
 (mbe
   :logic (sd-problem type priority groupsize key ctx)
   :exec (hons :sd-problem (hons (hons type priority)
                                 (hons groupsize (hons key ctx))))))