Lines Matching defs:package
1 (in-package "ACL2")
4 ; filenames corresponding representations (Lisp and ML) of the current package
11 ; resulting symbol's package name is actual-pkg-name. That is, the symbol with
12 ; name symbol-name and package-name actual-pkg-name is imported into package
13 ; known-pkg-name. The second form is a list of known package names. Note that
34 (symbol-package-name (car imports)))
43 (package-entry-name (car kpa))
44 (package-entry-imports (car kpa))
101 (name (package-entry-name entry))
102 (imports (package-entry-imports entry)))
114 (known-package-alist state))
123 (kpa (known-package-alist state))
138 (loop for x in (kpa-to-triples (known-package-alist state) nil)
139 when (not (equal (symbol-package-name (intern (car x) (cadr x))) (caddr x)))
143 ; Now we check that the current known-package-alist agrees with the
144 ; known-package-alist from a given lisp file, such as was written above.
146 (defun chk-known-package-alist (pkg-file state)
147 (let ((ctx 'chk-known-package-alist))
153 "Unexpected form for package file, ~x0."
158 (imports-alist-from-kpa (known-package-alist state)))
164 "Known package~#0~[ ~&0 is~/s ~&0 are~] is ~
165 missing in package file ~x1."
169 (fms "Chk-known-package-alist: PASSED~|"
181 the known-package-alist stored in file ~x1. ~
183 into package ~x2, as follows.~|~%For the ~
184 current known-package-alist:~| ~
186 '(known-package-alist state)
193 (defun note-chk-known-package-alist-success (filename state)
198 (er soft 'note-chk-known-package-alist-success