Filtering...

pseudo-lambdap-tests

books/std/system/pseudo-lambdap-tests

Included Books

pseudo-lambdap assert-bang must-succeed-star
other
(in-package "ACL2")
include-book
(include-book "pseudo-lambdap")
include-book
(include-book "std/testing/assert-bang" :dir :system)
include-book
(include-book "std/testing/must-succeed-star" :dir :system)
other
(assert! (not (pseudo-lambdap "abc")))
other
(assert! (not (pseudo-lambdap (cons 3 6))))
other
(assert! (not (pseudo-lambdap '(lambda (x) x extra))))
other
(assert! (not (pseudo-lambdap '(lambd (x) x))))
other
(assert! (not (pseudo-lambdap '(lambda (x 8) x))))
other
(assert! (not (pseudo-lambdap '(lambda (x y) #\a))))
other
(assert! (pseudo-lambdap '(lambda (x) x)))
other
(assert! (pseudo-lambdap '(lambda (x y z) (+ x (* y z)))))
other
(assert! (pseudo-lambdap '(lambda (x y z) (+ x x))))
other
(assert! (pseudo-lambdap '(lambda (x y z) (+ a b))))
other
(must-succeed* (defconst *term* '((lambda (x) (1+ x)) y))
  (assert! (pseudo-termp *term*))
  (assert! (pseudo-lambdap (ffn-symb *term*))))