		Search-engine friendly clone of the ACL2 documentation.

Unicode-input-char

Change-unicode-input-char

Modifying constructor for unicode-input-char structures.

Syntax

(change-unicode-input-char x 
                           [:unicode <unicode>] 
                           [:umarker <umarker>])

This is an often useful alternative to make-unicode-input-char.

We construct a new unicode-input-char 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-unicode-input-char

(defmacro change-unicode-input-char (x &rest args)
  (std::change-aggregate 'unicode-input-char
                         x args
                         '((:unicode . unicode-input-char->unicode)
                           (:umarker . unicode-input-char->umarker))
                         'change-unicode-input-char
                         'nil))