		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-collect-idents

Ident-option-collect-idents

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

Definitions and Theorems

Function: ident-option-collect-idents

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

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

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

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

(defthm ident-option-collect-idents-of-ident-option-fix-ident-option
  (equal
       (ident-option-collect-idents (ident-option-fix ident-option))
       (ident-option-collect-idents ident-option)))

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

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