		Search-engine friendly clone of the ACL2 documentation.

Ringosc3

Change-ringosc3

Modifying constructor for ringosc3 structures.

Syntax

(change-ringosc3 x 
                 [:n1 <n1>] 
                 [:n2 <n2>] 
                 [:n3 <n3>] 
                 [:inv1 <inv1>] 
                 [:inv2 <inv2>] 
                 [:inv3 <inv3>])

This is an often useful alternative to make-ringosc3.

We construct a new ringosc3 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-ringosc3

(defmacro change-ringosc3 (x &rest args)
  (std::change-aggregate 'ringosc3
                         x args
                         '((:n1 . ringosc3->n1)
                           (:n2 . ringosc3->n2)
                           (:n3 . ringosc3->n3)
                           (:inv1 . ringosc3->inv1)
                           (:inv2 . ringosc3->inv2)
                           (:inv3 . ringosc3->inv3))
                         'change-ringosc3
                         'nil))