		Search-engine friendly clone of the ACL2 documentation.

Defmapping-infop

Change-defmapping-info

A copying macro that lets you create new defmapping-infop structures, based on existing structures.

Syntax:

(change-defmapping-info x 
                        [:call$ <call$>] 
                        [:expansion <expansion>] 
                        [:doma <doma>] 
                        [:domb <domb>] 
                        [:alpha <alpha>] 
                        [:beta <beta>] 
                        [:alpha-image <alpha-image>] 
                        [:beta-image <beta-image>] 
                        [:beta-of-alpha <beta-of-alpha>] 
                        [:alpha-of-beta <alpha-of-beta>] 
                        [:alpha-injective <alpha-injective>] 
                        [:beta-injective <beta-injective>] 
                        [:doma-guard <doma-guard>] 
                        [:domb-guard <domb-guard>] 
                        [:alpha-guard <alpha-guard>] 
                        [:beta-guard <beta-guard>] 
                        [:unconditional <unconditional>])

This is a sometimes useful alternative to make-defmapping-info. It constructs a new defmapping-infop 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-defmapping-info

(defmacro change-defmapping-info (x &rest args)
  (std::change-aggregate
       'defmapping-info
       x args
       '((:call$ . defmapping-info->call$)
         (:expansion . defmapping-info->expansion)
         (:doma . defmapping-info->doma)
         (:domb . defmapping-info->domb)
         (:alpha . defmapping-info->alpha)
         (:beta . defmapping-info->beta)
         (:alpha-image . defmapping-info->alpha-image)
         (:beta-image . defmapping-info->beta-image)
         (:beta-of-alpha . defmapping-info->beta-of-alpha)
         (:alpha-of-beta . defmapping-info->alpha-of-beta)
         (:alpha-injective . defmapping-info->alpha-injective)
         (:beta-injective . defmapping-info->beta-injective)
         (:doma-guard . defmapping-info->doma-guard)
         (:domb-guard . defmapping-info->domb-guard)
         (:alpha-guard . defmapping-info->alpha-guard)
         (:beta-guard . defmapping-info->beta-guard)
         (:unconditional . defmapping-info->unconditional))
       'change-defmapping-info
       'nil))