Major Section: ACL2-BUILT-INS
(Char s n) is the
nth element of
s, zero-based. If
greater than or equal to the length of
(Char s n) has a guard that
n is a non-negative integer and
s is a
Char is a Common Lisp function. See any Common Lisp documentation
for more information.
To see the ACL2 definition of this function, see pf.