Map an optional expression to an optional expression in the language definition.
(ldm-expr-option expr?) → (mv erp expr?1)
Function:
(defun ldm-expr-option (expr?) (declare (xargs :guard (expr-optionp expr?))) (declare (xargs :guard (expr-option-unambp expr?))) (let ((__function__ 'ldm-expr-option)) (declare (ignorable __function__)) (b* (((reterr) nil)) (expr-option-case expr? :some (ldm-expr expr?.val) :none (retok nil)))))
Theorem:
(defthm expr-optionp-of-ldm-expr-option.expr?1 (b* (((mv acl2::?erp ?expr?1) (ldm-expr-option expr?))) (c::expr-optionp expr?1)) :rule-classes :rewrite)
Theorem:
(defthm ldm-expr-option-of-expr-option-fix-expr? (equal (ldm-expr-option (expr-option-fix expr?)) (ldm-expr-option expr?)))
Theorem:
(defthm ldm-expr-option-expr-option-equiv-congruence-on-expr? (implies (expr-option-equiv expr? expr?-equiv) (equal (ldm-expr-option expr?) (ldm-expr-option expr?-equiv))) :rule-classes :congruence)