books/workshops/2000/russinoff-kaufmann/supporting-materials/declarations.lisp


1
2
3
4
5
6
7
8
9
10
11

(in-package "*")

(encapsulate ; Input declarations.
 ((in () t)
  (longop () t))
 (local (defun in () 0))
 (local (defun longop () 0))
 (defthm acl2::input-spec-thm
   (and (bvecp (in) 4)
        (bvecp (longop) 1))
   :rule-classes ()))