Process the
Here we just check that it is a boolean
and that it is consistent with
Function:
(defun atj-process-no-aij-types (no-aij-types deep$ guards$ ctx state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (booleanp deep$) (booleanp guards$) (ctxp ctx)))) (let ((__function__ 'atj-process-no-aij-types)) (declare (ignorable __function__)) (b* (((er &) (ensure-value-is-boolean$ no-aij-types "The :NO-AIJ-TYPES input" t nil)) ((when (and no-aij-types deep$)) (er-soft+ ctx t nil "The :NO-AIJ-TYPES input may be T ~ only if :DEEP is NIL, but :DEEP is T instead.")) ((when (and no-aij-types (not guards$))) (er-soft+ ctx t nil "The :NO-AIJ-TYPES input may be T ~ only if :GUARDS is T, but :GUARDS is NIL instead."))) (value nil))))
Theorem:
(defthm null-of-atj-process-no-aij-types.nothing (b* (((mv ?erp ?nothing acl2::?state) (atj-process-no-aij-types no-aij-types deep$ guards$ ctx state))) (null nothing)) :rule-classes :rewrite)