		Search-engine friendly clone of the ACL2 documentation.

Ienv

Change-ienv

Modifying constructor for ienv structures.

Syntax

(change-ienv x 
             [:short-bytes <short-bytes>] 
             [:int-bytes <int-bytes>] 
             [:long-bytes <long-bytes>] 
             [:llong-bytes <llong-bytes>] 
             [:plain-char-signedp <plain-char-signedp>])

This is an often useful alternative to make-ienv.

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

(defmacro change-ienv (x &rest args)
  (std::change-aggregate
       'ienv
       x args
       '((:short-bytes . ienv->short-bytes)
         (:int-bytes . ienv->int-bytes)
         (:long-bytes . ienv->long-bytes)
         (:llong-bytes . ienv->llong-bytes)
         (:plain-char-signedp . ienv->plain-char-signedp))
       'change-ienv
       'nil))