Remove a parameter from a list of parameter declarations.
(paramdecl-list-remove-param-by-ident params param-to-remove) → (mv success new-params removed-param)
Function:
(defun paramdecl-list-remove-param-by-ident (params param-to-remove) (declare (xargs :guard (and (paramdecl-listp params) (identp param-to-remove)))) (let ((__function__ 'paramdecl-list-remove-param-by-ident)) (declare (ignorable __function__)) (b* ((params (paramdecl-list-fix params)) ((when (endp params)) (mv nil params (c$::irr-paramdecl))) (param (first params)) (param-name (ident-from-paramdecl param)) ((when (equal param-name param-to-remove)) (mv t (rest params) param)) ((mv success new-params removed-param) (paramdecl-list-remove-param-by-ident (rest params) param-to-remove))) (mv success (cons param new-params) removed-param))))
Theorem:
(defthm booleanp-of-paramdecl-list-remove-param-by-ident.success (b* (((mv ?success ?new-params ?removed-param) (paramdecl-list-remove-param-by-ident params param-to-remove))) (booleanp success)) :rule-classes :rewrite)
Theorem:
(defthm paramdecl-listp-of-paramdecl-list-remove-param-by-ident.new-params (b* (((mv ?success ?new-params ?removed-param) (paramdecl-list-remove-param-by-ident params param-to-remove))) (paramdecl-listp new-params)) :rule-classes :rewrite)
Theorem:
(defthm paramdeclp-of-paramdecl-list-remove-param-by-ident.removed-param (b* (((mv ?success ?new-params ?removed-param) (paramdecl-list-remove-param-by-ident params param-to-remove))) (paramdeclp removed-param)) :rule-classes :rewrite)