(call-graph-expr-option expr? fn-name acc) → call-graph
Function:
(defun call-graph-expr-option (expr? fn-name acc) (declare (xargs :guard (and (expr-optionp expr?) (identp fn-name) (ident-ident-option-set-mapp acc)))) (let ((__function__ 'call-graph-expr-option)) (declare (ignorable __function__)) (expr-option-case expr? :some (call-graph-expr expr?.val fn-name acc) :none (ident-ident-option-set-map-fix acc))))
Theorem:
(defthm ident-ident-option-set-mapp-of-call-graph-expr-option (b* ((call-graph (call-graph-expr-option expr? fn-name acc))) (ident-ident-option-set-mapp call-graph)) :rule-classes :rewrite)