Lines Matching defs:form
18 (defun expand-form (form untrans-flg state)
19 (declare (xargs :guard (true-listp form)))
21 (event-type (car form))
23 ((defun defund) (car (last form)))
24 ((defaxiom defthm defthmd) (third form)))))
33 (cadr form)
34 (caddr form)
37 (cadr form)
39 (otherwise (er hard 'expand-form
40 "Unexpected form type: ~x0"
41 form))))))))
72 (let ((form (car forms)))
73 (cond ((atom form) (value acc))
74 (t (case (car form)
77 (er-let* ((defs (expand-forms (cdr form) nil
84 (cons (cons (car form)
89 ((null (cadr form))
90 (expand-forms (cddr form) acc untrans-flg
99 (chk-signatures (cadr form) ctx wrld
101 (forms (expand-forms (cddr form) nil untrans-flg
111 (member-eq (car form) '(defun defund))
112 (eq (symbol-class (cadr form) (w state))
116 ((x (expand-form form untrans-flg state)))
120 (value (cons form acc))))))))))