Lines Matching defs:check
1 ;;; Given a file, check that each of its forms is essentially redundant. Here,
3 ;;; Thus, we might include an ACL2 book and then check that the resulting
8 ; (include-book "~/projects/HOL/examples/acl2/lisp/check-file")
10 ; (check-file "~/Downloads/pkg_test.lisp")
44 (defun check-form (form ctx wrld state)
106 (defun check-form-lst (lst ignore-errors ctx wrld state)
110 (check-form (car lst) ctx wrld state)
114 (t (check-form-lst (cdr lst) ignore-errors ctx wrld
117 (defun check-file1 (infile ignore-errors state)
118 (let ((ctx 'check-file)
122 (check-form-lst forms ignore-errors ctx wrld state))))
124 (defmacro check-file (infile &optional (show-all 't))
125 `(check-file1 ,infile ,show-all state))