		Search-engine friendly clone of the ACL2 documentation.

Svex-simplify

4vec-to-svex

Try to convert a term composed of 4vec functions to its equivalent svex representation.

Signature
(4vec-to-svex term svexl-node-flg memoize-flg) → (mv err res)

Function: 4vec-to-svex-memoize-condition

(defun 4vec-to-svex-memoize-condition
       (term svexl-node-flg memoize-flg)
       (declare (ignorable term svexl-node-flg memoize-flg)
                (xargs :guard 't))
       memoize-flg)

Theorem: svexl-node-p-of-4vec-to-svex

(defthm svexl-node-p-of-4vec-to-svex
        (b* (((mv ?err ?res)
              (4vec-to-svex term svexl-node-flg memoize-flg)))
            (and (svexl-node-p res)
                 (implies (not svexl-node-flg)
                          (svex-p res)))))

Theorem: svexl-nodelist-p-of-4vec-to-svex-lst

(defthm svexl-nodelist-p-of-4vec-to-svex-lst
        (b* (((mv ?err ?res-lst)
              (4vec-to-svex-lst lst svexl-node-flg memoize-flg)))
            (and (svexl-nodelist-p res-lst)
                 (implies (not svexl-node-flg)
                          (svexlist-p res-lst)))))

Subtopics

4vec-to-svex-lst