		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