		Search-engine friendly clone of the ACL2 documentation.

Sd-problem-p

Sd-problem

Raw constructor for sd-problem-p structures.

Syntax:

(sd-problem type priority groupsize key ctx)

This is the lowest-level constructor for sd-problem-p structures. It simply conses together a structure with the specified fields.

Note: It's generally better to use macros like make-sd-problem or change-sd-problem instead. These macros lead to more readable and robust code, because you don't have to remember the order of the fields.

The sd-problem-p structures we create here are just constructed with ordinary cons. If you want to create honsed structures, see honsed-sd-problem instead.

Definition

This is an ordinary constructor function introduced by defaggregate.

Function: sd-problem

(defun 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))))
  (cons :sd-problem (cons (cons type priority)
                          (cons groupsize (cons key ctx)))))