Post #4404268
2026-08-05 05:13 UTC
@ramin_hal9001@fe.disroot.org Whence we can see:
$ cert.pl ./stobj.lisp
$ acl2
ACL2 !>(include-book "stobj")
ACL2 !>(add-word words "hello")
( ("hello"))
ACL2 !>(add-word words "world")
( ("hello" "world"))
acl2 describes stobjs as taking the draconian approach that stobjs are so syntactically restricted that it is unambiguous that there is only ever one state. In practice, any access to a stobj must return that stobj (i.e. with mv ~ values).
Replies (1)
-
@screwlisp@gamerplus.org 2026-08-05 05:26
@ramin_hal9001@fe.disroot.org A lisp struct: CLIM-USER> (defstruct (words (:conc-name wr-)) (words-seen () :type t)) WORDS CLIM-USER> (defun add-word (words word) (values words (setf (wr-words-seen words) (append (wr-words-seen words) (list word))))) ADD-WORD CLIM-USER> #S(words) #S(WORDS :WORDS-SEEN NIL) CLIM-USER> (add-word * 'hello) #S(WORDS :WORDS-SEEN (HELLO)) (HELLO) CLIM-USER> (add-word * 'world) #S(WORDS :WORDS-SEEN (HELLO WORLD)) (HELLO WORLD)