- To make Ivy work in ACL2-2.6 and ACL2-2.7, in the book paramod.lisp
(defthm len-0-list-forward
(implies (and (true-listp l)
(equal (+ n (len l)) n))
(equal l nil))
:rule-classes :forward-chaining)
should be replaced by
(defthm len-0-list-forward
(implies (and (true-listp l)
(equal (len l) 0))
(equal l nil))
:rule-classes :forward-chaining)