		Search-engine friendly clone of the ACL2 documentation.

Symbolic-arithmetic

Syntactically-true-p

Signature
(syntactically-true-p x) → true-p
Returns: true-p — Type (booleanp true-p).

Definitions and Theorems

Function: syntactically-true-p

(defun syntactically-true-p (x)
  (declare (xargs :guard t))
  (let ((__function__ 'syntactically-true-p))
    (declare (ignorable __function__))
    (eq x t)))

Theorem: booleanp-of-syntactically-true-p

(defthm booleanp-of-syntactically-true-p
  (b* ((true-p (syntactically-true-p x)))
    (booleanp true-p))
  :rule-classes :rewrite)

Theorem: syntactically-true-p-implies

(defthm syntactically-true-p-implies
  (b* nil
    (implies (syntactically-true-p x)
             (equal (bfr-eval x env) t))))

Theorem: syntactically-true-p-rewrite

(defthm syntactically-true-p-rewrite
 (b* nil
  (implies
   (and
       (acl2::rewriting-negative-literal (cons 'syntactically-true-p
                                               (cons x 'nil)))
       (bind-free '((env . env)) (env)))
   (iff (syntactically-true-p x)
        (and (equal (bfr-eval x env) t)
             (hide (syntactically-true-p x)))))))