		Search-engine friendly clone of the ACL2 documentation.

4vs-t

(4vs-t) returns (T), the s-expression for a constant true value.

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

Function: 4vs-t$inline

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

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

(defthm 4v-sexpr-eval-of-4vs-t
  (equal (4v-sexpr-eval (4vs-t) env)
         (4vt)))

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

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