tbh I'm not sure why #acl2 doesn't have getf. Here is my "do-loop$" loopy one. #commonLisp
ACL2 !>(forgetf :a '(:c d :a b))
B
~
(defun forgetf (key plist)
(loop$ with pl of-type list = plist
do
(cond ((null pl) (return nil))
((equal key (car pl))
(return (cadr pl)))
(t (setq pl (cddr pl))))))
Allowing, this proof is vacuous, but you can check theorems about pretty normal #lisp code:
(thm
(implies
(and
(equal plist '(:a 1 :b 2))
(equal key :b)
(equal x (forgetf key plist)))
(evenp x)))
..
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted: 112
Proof succeeded.
( forgetf is an admitted function; if you call it on the values given, what it returns is evenp).
https://lispy-gopher-show.itch.io/lispmoo2/devlog/1481398/homespun-acl2-handler-bind-condition-handling #acl2 simple introduction to acl2 for the #commonLisp inclined. loop$, apply$, thms oh my. In particular, I implement a model of a simple case of the common lisp condition system that is directly compatible with both ansi common lisp and acl2. (a computational logic for applicative common lisp). #firstOrderLogic #theoremProving #programming #logic #example Technically this is in support of my lisp / moo compatibility layer but I am not going to beleaguer the tag.
screwlisp