|
|
|---|
|
|
|
|---|
Raw constructor for eqbylbp-config-p structures.
Syntax:
(eqbylbp-config restriction witness-rule
instance-rule prune-examples
passes simp-hint add-hints verbosep)This is the lowest-level constructor for eqbylbp-config-p structures. It simply conses together a structure with the specified fields.
Note: It's generally better to use macros like make-eqbylbp-config or change-eqbylbp-config instead. These macros lead to more readable and robust code, because you don't have to remember the order of the fields.
The eqbylbp-config-p structures we create here are just constructed with ordinary cons. If you want to create honsed structures, see honsed-eqbylbp-config instead.
This is an ordinary constructor function introduced by defaggregate.
Function:
(defun eqbylbp-config (restriction witness-rule instance-rule prune-examples passes simp-hint add-hints verbosep) (declare (xargs :guard (and (pseudo-termp restriction) (acl2::wcp-witness-rule-p witness-rule) (and (acl2::wcp-instance-rule-p instance-rule) (equal (len (acl2::wcp-instance-rule->vars instance-rule)) 1)) (posp passes)))) (cons (cons 'restriction restriction) (cons (cons 'witness-rule witness-rule) (cons (cons 'instance-rule instance-rule) (cons (cons 'prune-examples prune-examples) (cons (cons 'passes passes) (cons (cons 'simp-hint simp-hint) (cons (cons 'add-hints add-hints) (cons (cons 'verbosep verbosep) nil)))))))))