		Search-engine friendly clone of the ACL2 documentation.

4vs-f

(4vs-f) returns (F), the s-expression for a constant false value.

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

Function: 4vs-f$inline

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

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

(defthm 4v-sexpr-eval-of-4vs-f
  (equal (4v-sexpr-eval (4vs-f) env)
         (4vf)))

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

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