(abs-primary-expression-alt2 tree) → expr
Function:
(defun abs-primary-expression-alt2 (tree) (declare (xargs :guard (abnf::treep tree))) (declare (xargs :guard (cst-matchp tree "primary-expression"))) (let ((__function__ 'abs-primary-expression-alt2)) (declare (ignorable __function__)) (case (cst-primary-expression-conc? tree) (1 (make-expression-var :name (abs-identifier-alt (cst-primary-expression-conc1-rep-elem tree)))) (2 (make-expression-const :value (abs-integer-alt (cst-primary-expression-conc2-rep-elem tree)))))))
Theorem:
(defthm expressionp-of-abs-primary-expression-alt2 (b* ((expr (abs-primary-expression-alt2 tree))) (expressionp expr)) :rule-classes :rewrite)
Theorem:
(defthm abs-primary-expression-alt2-of-tree-fix-tree (equal (abs-primary-expression-alt2 (abnf::tree-fix tree)) (abs-primary-expression-alt2 tree)))
Theorem:
(defthm abs-primary-expression-alt2-tree-equiv-congruence-on-tree (implies (abnf::tree-equiv tree tree-equiv) (equal (abs-primary-expression-alt2 tree) (abs-primary-expression-alt2 tree-equiv))) :rule-classes :congruence)