|
|
|---|
|
|
|
|---|
Raw constructor for honsed token-p structures.
Syntax:
(honsed-token type text)
This is identical to token, except that we hons the structure we are creating.
This is an ordinary honsing constructor introduced by defaggregate.
Function:
(defun honsed-token (type text) (declare (xargs :guard (and (tokentype-p type) (stringp text)))) (mbe :logic (token type text) :exec (hons type text)))