Filtering...

term-guard-obligation-tests

books/std/system/term-guard-obligation-tests

Included Books

term-guard-obligation assert-equal
other
(in-package "ACL2")
include-book
(include-book "term-guard-obligation")
include-book
(include-book "std/testing/assert-equal" :dir :system)
other
(assert-equal (term-guard-obligation 'x t state) ''t)
other
(assert-equal (term-guard-obligation 'x :limited state) ''t)
other
(assert-equal (term-guard-obligation '(binary-+ x '4) t state)
  '(acl2-numberp x))
other
(assert-equal (term-guard-obligation '(binary-+ x '4) :limited state)
  '(acl2-numberp x))
other
(assert-equal (term-guard-obligation '(< (len x) '17) t state)
  ''t)
other
(assert-equal (term-guard-obligation '(< (len x) '17) :limited state)
  '(rationalp (len x)))