Language.ACL2

data Expr

check

check'

mutualRecursion

defun

defun'

defconst

defthm

thm

call

obj

quote

consp

cons

car

cdr

nth

len

take'

nthcdr

updateNth

append

let'

if'

case'

assoc

var

list

lit

string

nil

t

zp

zip'

undefined'

equal

not'

and'

or'

implies

goodbye

integerp

mod'

(<.)

(>.)

(<=.)

(>=.)