Filtering...

genvar-dollar-tests

books/std/system/genvar-dollar-tests

Included Books

genvar-dollar assert-equal
other
(in-package "ACL2")
include-book
(include-book "genvar-dollar")
include-book
(include-book "std/testing/assert-equal" :dir :system)
other
(assert-equal (genvar (pkg-witness "ACL2") "VAR" nil nil)
  'var)
other
(assert-equal (genvar (pkg-witness "ACL2") "VAR" nil '(var))
  'var0)
other
(assert-equal (genvar (pkg-witness "ACL2-USER") "XYZ" 17 '(var))
  'xyz17)
other
(assert-equal (genvar (pkg-witness "ACL2-USER")
    "XYZ"
    17
    '(xyz17 xyz18))
  'xyz19)