		Search-engine friendly clone of the ACL2 documentation.

Strin-p

Honsed-strin

Raw constructor for honsed strin-p structures.

Syntax:

(honsed-strin chars line col file)

This is identical to strin, except that we hons the structure we are creating.

Definition

This is an ordinary honsing constructor introduced by defaggregate.

Function: honsed-strin

(defun honsed-strin (chars line col file)
 (declare (xargs :guard (and (character-listp chars)
                             (posp line)
                             (natp col)
                             (stringp file))))
 (mbe
   :logic (strin chars line col file)
   :exec
   (hons :strin (hons (hons 'chars chars)
                      (hons (hons 'line line)
                            (hons (hons 'col col)
                                  (hons (hons 'file file) nil)))))))