		Search-engine friendly clone of the ACL2 documentation.

4vs-x

(4vs-x) returns (X), the s-expression for a constant unknown value.

This is potentially nicer than using *4vx-sexpr* directly because it can be disabled so that rules about cons will not apply.

Function: 4vs-x$inline

(defun 4vs-x$inline nil
  (declare (xargs :guard t))
  *4vx-sexpr*)

Theorem: 4v-sexpr-eval-of-4vs-x

(defthm 4v-sexpr-eval-of-4vs-x
  (equal (4v-sexpr-eval (4vs-x) env)
         (4vx)))

Theorem: 4v-sexpr-vars-of-4vs-x

(defthm 4v-sexpr-vars-of-4vs-x
  (equal (4v-sexpr-vars (4vs-x)) nil))