		Search-engine friendly clone of the ACL2 documentation.

4vs-z

(4vs-z) returns (Z), the s-expression for a constant undriven/floating value.

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

Function: 4vs-z$inline

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

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

(defthm 4v-sexpr-eval-of-4vs-z
  (equal (4v-sexpr-eval (4vs-z) env)
         (4vz)))

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

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