		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-unambp

Fundef-option-unambp

Signature
(fundef-option-unambp fundef-option) → fty::result
Arguments: fundef-option — Guard (fundef-optionp fundef-option).
Returns: fty::result — Type (booleanp fty::result).

Definitions and Theorems

Function: fundef-option-unambp

(defun fundef-option-unambp (fundef-option)
 (declare (xargs :guard (fundef-optionp fundef-option)))
 (let ((__function__ 'fundef-option-unambp))
  (declare (ignorable __function__))
  (fundef-option-case
       fundef-option
       :some (fundef-unambp (fundef-option-some->val fundef-option))
       :none t)))

Theorem: booleanp-of-fundef-option-unambp

(defthm booleanp-of-fundef-option-unambp
  (b* ((fty::result (fundef-option-unambp fundef-option)))
    (booleanp fty::result))
  :rule-classes :rewrite)

Theorem: fundef-option-unambp-of-fundef-option-fix-fundef-option

(defthm fundef-option-unambp-of-fundef-option-fix-fundef-option
  (equal (fundef-option-unambp (fundef-option-fix fundef-option))
         (fundef-option-unambp fundef-option)))

Theorem: fundef-option-unambp-fundef-option-equiv-congruence-on-fundef-option

(defthm
 fundef-option-unambp-fundef-option-equiv-congruence-on-fundef-option
 (implies (fundef-option-equiv fundef-option fundef-option-equiv)
          (equal (fundef-option-unambp fundef-option)
                 (fundef-option-unambp fundef-option-equiv)))
 :rule-classes :congruence)