		Search-engine friendly clone of the ACL2 documentation.

Lhprobe-constraint

Change-lhprobe-constraint

Modifying constructor for lhprobe-constraint structures.

Syntax

(change-lhprobe-constraint x 
                           [:lhprobe <lhprobe>] 
                           [:val <val>])

This is an often useful alternative to make-lhprobe-constraint.

We construct a new lhprobe-constraint structure that is a copy of x, except that you can explicitly change some particular fields. Any fields you don't mention just keep their values from x.

Definition

This is an ordinary change- macro introduced by defprod.

Macro: change-lhprobe-constraint

(defmacro change-lhprobe-constraint (x &rest args)
  (std::change-aggregate 'lhprobe-constraint
                         x args
                         '((:lhprobe . lhprobe-constraint->lhprobe)
                           (:val . lhprobe-constraint->val))
                         'change-lhprobe-constraint
                         'remake-lhprobe-constraint))