		Search-engine friendly clone of the ACL2 documentation.

Ipasir$a

Change-ipasir$a

Modifying constructor for ipasir$a structures.

Syntax

(change-ipasir$a x 
                 [:formula <formula>] 
                 [:assumption <assumption>] 
                 [:new-clause <new-clause>] 
                 [:status <status>] 
                 [:solution <solution>] 
                 [:solved-assumption <solved-assumption>] 
                 [:callback-count <callback-count>] 
                 [:history <history>])

This is an often useful alternative to make-ipasir$a.

We construct a new ipasir$a 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 fty::defprod.

Macro: change-ipasir$a

(defmacro change-ipasir$a (x &rest args)
  (std::change-aggregate
       'ipasir$a
       x args
       '((:formula . ipasir$a->formula)
         (:assumption . ipasir$a->assumption)
         (:new-clause . ipasir$a->new-clause)
         (:status . ipasir$a->status)
         (:solution . ipasir$a->solution)
         (:solved-assumption . ipasir$a->solved-assumption)
         (:callback-count . ipasir$a->callback-count)
         (:history . ipasir$a->history))
       'change-ipasir$a
       'nil))