		Search-engine friendly clone of the ACL2 documentation.

Func

Change-func

Modifying constructor for func structures.

Syntax

(change-func x 
             [:name <name>] 
             [:formals <formals>] 
             [:guard <guard>] 
             [:returns <returns>] 
             [:more-returns <more-returns>] 
             [:expansion-depth <expansion-depth>] 
             [:flattened-formals <flattened-formals>] 
             [:flattened-returns <flattened-returns>])

This is an often useful alternative to make-func.

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

(defmacro change-func (x &rest args)
  (std::change-aggregate
       'func
       x args
       '((:name . func->name)
         (:formals . func->formals)
         (:guard . func->guard)
         (:returns . func->returns)
         (:more-returns . func->more-returns)
         (:expansion-depth . func->expansion-depth)
         (:flattened-formals . func->flattened-formals)
         (:flattened-returns . func->flattened-returns))
       'change-func
       'nil))