		Search-engine friendly clone of the ACL2 documentation.

Expdata-surjmapp

Change-expdata-surjmap

A copying macro that lets you create new expdata-surjmapp structures, based on existing structures.

Syntax:

(change-expdata-surjmap x 
                        [:surjname <surjname>] 
                        [:localp <localp>] 
                        [:oldp <oldp>] 
                        [:newp <newp>] 
                        [:forth <forth>] 
                        [:back <back>] 
                        [:forth-image <forth-image>] 
                        [:back-image <back-image>] 
                        [:back-of-forth <back-of-forth>] 
                        [:forth-injective <forth-injective>] 
                        [:oldp-guard <oldp-guard>] 
                        [:newp-guard <newp-guard>] 
                        [:forth-guard <forth-guard>] 
                        [:back-guard <back-guard>] 
                        [:hints <hints>])

This is a sometimes useful alternative to make-expdata-surjmap. It constructs a new expdata-surjmapp 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 std::defaggregate.

Macro: change-expdata-surjmap

(defmacro change-expdata-surjmap (x &rest args)
  (std::change-aggregate
       'expdata-surjmap
       x args
       '((:surjname . expdata-surjmap->surjname)
         (:localp . expdata-surjmap->localp)
         (:oldp . expdata-surjmap->oldp)
         (:newp . expdata-surjmap->newp)
         (:forth . expdata-surjmap->forth)
         (:back . expdata-surjmap->back)
         (:forth-image . expdata-surjmap->forth-image)
         (:back-image . expdata-surjmap->back-image)
         (:back-of-forth . expdata-surjmap->back-of-forth)
         (:forth-injective . expdata-surjmap->forth-injective)
         (:oldp-guard . expdata-surjmap->oldp-guard)
         (:newp-guard . expdata-surjmap->newp-guard)
         (:forth-guard . expdata-surjmap->forth-guard)
         (:back-guard . expdata-surjmap->back-guard)
         (:hints . expdata-surjmap->hints))
       'change-expdata-surjmap
       'nil))