other
(in-package "GL")
other
(include-book "generic-geval")
other
(include-book "symbolic-arithmetic")
other
(def-eval-g eval-g-base
(binary-* cons
if
binary-+
pkg-witness
unary--
complex-rationalp
acl2-numberp
symbol-package-name
intern-in-package-of-symbol
code-char
denominator
cdr
car
consp
symbol-name
char-code
imagpart
symbolp
realpart
numerator
equal
stringp
rationalp
cons
integerp
characterp
<
coerce
booleanp
logbitp
binary-logand
binary-logior
binary-logxor
binary-logeqv
lognot
ash
integer-length
floor
mod
truncate
rem
bool-fix$inline
bool->bit$inline
bool->sign
hons-assoc-equal
not
implies
eq
atom
eql
=
/=
null
endp
zerop
plusp
minusp
listp
logapp
int-set-sign
maybe-integer
binary-minus-for-gl))
other
(in-theory (disable eval-g-base))