check-equal

(defun fcheck
  (form state)
  (declare (xargs :mode :program :stobjs (state)))
  (b* (((er res) (with-output! :on error
         (trans-eval form 'check state t))) ((when (not (equal (cdr res) t))) (prog2$ (cw "~%ACL2s Error in CHECK: The form evaluates to: ~x0, not T!~%"
            (cdr res))
          (mv t nil state))))
    (value '(value-triple :passed))))

(defun fcheck=
  (form1 form2 state)
  (declare (xargs :mode :program :stobjs (state)))
  (b* (((er res1) (with-output! :on error
         (trans-eval form1
           'check=
           state
           t))) ((er res2) (with-output! :on error
          (trans-eval form2
            'check=
            state
            t)))
      ((when (not (equal (car res1) (car res2)))) (prog2$ (cw "~%ACL2s Error in CHECK=: The forms return a different number or stobj types.~%")
          (mv t nil state)))
      ((when (not (equal (cdr res1) (cdr res2)))) (prog2$ (cw "~%ACL2s Error in CHECK=: Check failed (values not equal).~
               ~%First value:  ~x0~
               ~%Second value: ~x1~%"
            (cdr res1)
            (cdr res2))
          (mv t nil state))))
    (value '(value-triple :passed))))