		Search-engine friendly clone of the ACL2 documentation.

Split-fn-when-implementation

Ext-declon-list-try-split-fn-when

Signature
(ext-declon-list-try-split-fn-when extdecls triggers transunits) → (mv er? found extdecls$)
Arguments: extdecls — Guard (ext-declon-listp extdecls).; triggers — Guard (ident-setp triggers).; transunits — Guard (transunit-ensemblep transunits).
Returns: er? — Type (maybe-msgp er?).; found — Type (booleanp found).; extdecls$ — Type (ext-declon-listp extdecls$).

Definitions and Theorems

Function: ext-declon-list-try-split-fn-when

(defun ext-declon-list-try-split-fn-when
       (extdecls triggers transunits)
  (declare (xargs :guard (and (ext-declon-listp extdecls)
                              (ident-setp triggers)
                              (transunit-ensemblep transunits))))
  (b* (((reterr) nil nil)
       ((when (endp extdecls)) (retok nil nil))
       ((erp found extdecls1)
        (ext-declon-try-split-fn-when (first extdecls)
                                      triggers transunits))
       ((when found)
        (retok t
               (append extdecls1
                       (ext-declon-list-fix (rest extdecls)))))
       ((erp found extdecls2)
        (ext-declon-list-try-split-fn-when (rest extdecls)
                                           triggers transunits)))
    (retok found (append extdecls1 extdecls2))))

Theorem: maybe-msgp-of-ext-declon-list-try-split-fn-when.er?

(defthm maybe-msgp-of-ext-declon-list-try-split-fn-when.er?
  (b* (((mv ?er? ?found ?extdecls$)
        (ext-declon-list-try-split-fn-when
             extdecls triggers transunits)))
    (maybe-msgp er?))
  :rule-classes :rewrite)

Theorem: booleanp-of-ext-declon-list-try-split-fn-when.found

(defthm booleanp-of-ext-declon-list-try-split-fn-when.found
  (b* (((mv ?er? ?found ?extdecls$)
        (ext-declon-list-try-split-fn-when
             extdecls triggers transunits)))
    (booleanp found))
  :rule-classes :type-prescription)

Theorem: ext-declon-listp-of-ext-declon-list-try-split-fn-when.extdecls$

(defthm
    ext-declon-listp-of-ext-declon-list-try-split-fn-when.extdecls$
  (b* (((mv ?er? ?found ?extdecls$)
        (ext-declon-list-try-split-fn-when
             extdecls triggers transunits)))
    (ext-declon-listp extdecls$))
  :rule-classes :rewrite)

Theorem: true-listp-of-ext-declon-list-try-split-fn-when.extdecls$

(defthm true-listp-of-ext-declon-list-try-split-fn-when.extdecls$
  (b* (((mv ?er? ?found ?extdecls$)
        (ext-declon-list-try-split-fn-when
             extdecls triggers transunits)))
    (true-listp extdecls$))
  :rule-classes :type-prescription)