Filtering...

char-kinds-tests

books/std/strings/char-kinds-tests

Included Books

char-kinds assert-bang
other
(in-package "ACL2")
include-book
(include-book "char-kinds")
include-book
(include-book "std/testing/assert-bang" :dir :system)
other
(assert! (letter-char-p #\a))
other
(assert! (letter-char-p #\G))
other
(assert! (not (letter-char-p #\5)))
other
(assert! (letter/digit-char-p #\a))
other
(assert! (letter/digit-char-p #\G))
other
(assert! (letter/digit-char-p #\5))
other
(assert! (not (letter/digit-char-p #\-)))
other
(assert! (not (letter/digit-char-p #\\)))
other
(assert! (not (letter/digit-char-p #\<)))
other
(assert! (letter/digit/dash-char-p #\a))
other
(assert! (letter/digit/dash-char-p #\G))
other
(assert! (letter/digit/dash-char-p #\5))
other
(assert! (letter/digit/dash-char-p #\-))
other
(assert! (not (letter/digit/dash-char-p #\\)))
other
(assert! (not (letter/digit/dash-char-p #\<)))
other
(assert! (letter/digit/uscore-char-p #\a))
other
(assert! (letter/digit/uscore-char-p #\G))
other
(assert! (letter/digit/uscore-char-p #\5))
other
(assert! (letter/digit/uscore-char-p #\_))
other
(assert! (not (letter/digit/uscore-char-p #\\)))
other
(assert! (not (letter/digit/uscore-char-p #\<)))
other
(assert! (letter/digit/uscore/dollar-char-p #\a))
other
(assert! (letter/digit/uscore/dollar-char-p #\G))
other
(assert! (letter/digit/uscore/dollar-char-p #\5))
other
(assert! (letter/digit/uscore/dollar-char-p #\_))
other
(assert! (letter/digit/uscore/dollar-char-p #\$))
other
(assert! (not (letter/digit/uscore/dollar-char-p #\-)))
other
(assert! (not (letter/digit/uscore/dollar-char-p #\^)))
other
(assert! (letter/uscore/dollar-char-p #\a))
other
(assert! (letter/uscore/dollar-char-p #\G))
other
(assert! (letter/uscore/dollar-char-p #\_))
other
(assert! (letter/uscore/dollar-char-p #\$))
other
(assert! (not (letter/uscore/dollar-char-p #\5)))
other
(assert! (not (letter/uscore/dollar-char-p #\#)))
other
(assert! (not (letter/uscore/dollar-char-p #\<)))
other
(assert! (nondigit-char-p #\a))
other
(assert! (not (nondigit-char-p #\0)))
other
(assert! (printable-char-p #\a))
other
(assert! (printable-char-p #\Y))
other
(assert! (printable-char-p #\ ))
other
(assert! (printable-char-p #\())
other
(assert! (printable-char-p #\@))
other
(assert! (not (printable-char-p #\
)))
other
(assert! (not (printable-char-p #\	)))
other
(assert! (ucletter-char-p #\Y))
other
(assert! (not (ucletter-char-p #\y)))
other
(assert! (lcletter-char-p #\z))
other
(assert! (not (lcletter-char-p #\Z)))
other
(assert! (ucletter/digit-char-p #\Y))
other
(assert! (ucletter/digit-char-p #\4))
other
(assert! (not (ucletter/digit-char-p #\y)))
other
(assert! (lcletter/digit-char-p #\y))
other
(assert! (lcletter/digit-char-p #\4))
other
(assert! (not (lcletter/digit-char-p #\Y)))