|
|
|---|
|
|
|
|---|
Raw constructor for honsed eqbylbp-config-p structures.
Syntax:
(honsed-eqbylbp-config restriction witness-rule
instance-rule prune-examples
passes simp-hint add-hints verbosep)This is identical to eqbylbp-config, except that we hons the structure we are creating.
This is an ordinary honsing constructor introduced by defaggregate.
Function:
(defun honsed-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)))) (mbe :logic (eqbylbp-config restriction witness-rule instance-rule prune-examples passes simp-hint add-hints verbosep) :exec (hons (hons 'restriction restriction) (hons (hons 'witness-rule witness-rule) (hons (hons 'instance-rule instance-rule) (hons (hons 'prune-examples prune-examples) (hons (hons 'passes passes) (hons (hons 'simp-hint simp-hint) (hons (hons 'add-hints add-hints) (hons (hons 'verbosep verbosep) nil))))))))))