		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-collect-idents

Fundef-option-collect-idents

Signature
(fundef-option-collect-idents c$::fundef-option) → fty::result
Arguments: c$::fundef-option — Guard (fundef-optionp c$::fundef-option).
Returns: fty::result — Type (ident-setp fty::result).

Definitions and Theorems

Function: fundef-option-collect-idents

(defun fundef-option-collect-idents (c$::fundef-option)
  (declare (xargs :guard (fundef-optionp c$::fundef-option)))
  (let ((__function__ 'fundef-option-collect-idents))
    (declare (ignorable __function__))
    (fundef-option-case
         c$::fundef-option
         :some (fundef-collect-idents
                    (c$::fundef-option-some->val c$::fundef-option))
         :none nil)))

Theorem: ident-setp-of-fundef-option-collect-idents

(defthm ident-setp-of-fundef-option-collect-idents
  (b*
    ((fty::result (fundef-option-collect-idents c$::fundef-option)))
    (ident-setp fty::result))
  :rule-classes :rewrite)

Theorem: fundef-option-collect-idents-of-fundef-option-fix-fundef-option

(defthm
    fundef-option-collect-idents-of-fundef-option-fix-fundef-option
  (equal (fundef-option-collect-idents
              (c$::fundef-option-fix c$::fundef-option))
         (fundef-option-collect-idents c$::fundef-option)))

Theorem: fundef-option-collect-idents-fundef-option-equiv-congruence-on-fundef-option

(defthm
 fundef-option-collect-idents-fundef-option-equiv-congruence-on-fundef-option
 (implies
     (c$::fundef-option-equiv c$::fundef-option fundef-option-equiv)
     (equal (fundef-option-collect-idents c$::fundef-option)
            (fundef-option-collect-idents fundef-option-equiv)))
 :rule-classes :congruence)