Generate the name of the field with the given index in an mv class.
As explained in atj-gen-shallow-mv-class-name, we generate Java classes that represent mv values. These classes have non-private fields named after the indices (0-based) of the components of the mv values.
Currently we generate field names of the form
Function:
(defun atj-gen-shallow-mv-field-name (index) (declare (xargs :guard (natp index))) (let ((__function__ 'atj-gen-shallow-mv-field-name)) (declare (ignorable __function__)) (str::cat "$" (nat-to-dec-string index))))
Theorem:
(defthm stringp-of-atj-gen-shallow-mv-field-name (b* ((field-name (atj-gen-shallow-mv-field-name index))) (stringp field-name)) :rule-classes :rewrite)