		Search-engine friendly clone of the ACL2 documentation.

Split-fn-when-implementation

Ext-declon-try-split-fn-when

Signature
(ext-declon-try-split-fn-when extdecl triggers transunits) → (mv er? found extdecls)
Arguments: extdecl — Guard (ext-declonp extdecl).; 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-try-split-fn-when

(defun ext-declon-try-split-fn-when (extdecl triggers transunits)
  (declare (xargs :guard (and (ext-declonp extdecl)
                              (ident-setp triggers)
                              (transunit-ensemblep transunits))))
  (b* (((reterr) nil nil))
    (ext-declon-case
         extdecl :fundef
         (b* (((erp fundef1 fundef2)
               (fundef-try-split-fn-when
                    extdecl.fundef triggers transunits)))
           (fundef-option-case
                fundef2
                :some (retok t
                             (list (ext-declon-fundef fundef1)
                                   (ext-declon-fundef fundef2.val)))
                :none (retok nil
                             (list (ext-declon-fundef fundef1)))))
         :otherwise (retok nil (list (ext-declon-fix extdecl))))))

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

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

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

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

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

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

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

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