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