ACL2s reference

Types

Name	Recognizer	Description
all	allp	the ACL2s universe
atom	atom	atomic data: numbers, strings, ...
symbol	symbolp	symbols
boolean	booleanp	t or nil
bool	booleanp	only works with definec
rational	rationalp	rational numbers (we assume that all numbers are rationals, which is not technically true in ACL2s)
integer	integerp	integers
int	integerp	only works with definec
nat	natp	natural numbers (int >= 0)
pos	posp	positive integers (int > 0)
cons	consp	conses, constructed with cons
true-list	tlp, true-listp	true lists (nil terminated cons)
tl	tlp, true-listp	only works in definec
list	listp	conses or nil

Function signatures

Name	Contract	Description
if	All x All x All -> All	if test then else
equal	All x All -> Bool	checks if args are equal
implies	All x All -> Bool	implication
iff	All x All -> Bool	if and only if (Boolean equality)
xor	All x All -> Bool	xor (Boolean disequality)
binary-+	Rational x Rational -> Rational	addition
binary-*	Rational x Rational -> Rational	multiplication
<	Rational x Rational -> Bool	less than
unary--	Rational -> Rational	unary -
unary-/	Rational \ {0} -> Rational	unary /
expt	(Rational X Integer) \ {(0, i) : i < 0}	exponentiation
numerator	Rational -> Integer	numerator
denominator	Rational -> Pos	denominator
mod	Rational x Rational \ {0} -> Rational	modular arithmetic
ceiling	Rational x Rational \ {0} -> Integer	ceiling of quotient
floor	Rational x Rational \ {0} -> Integer	floor of quotient
evenp	Integer -> Bool	is the number even?
oddp	Integer -> Bool	is the number odd?
cons	All x All -> All	create a cons
car	List -> All	car of a list
cdr	List -> All	cdr of a list
head	Cons-> All	car of a cons (not builtin, see lecture notes)
tail	Cons -> All	cdr of a cons (not builtin, see lecture notes)
endp	List -> Bool	is list empty?
aapp	TL x TL -> TL	concatenate two lists (not builtin, see lecture notes)
binary-append	TL x All -> All	concatenation
rev	ALL -> TL	reverse
rrev	TL -> TL	reverse a list (not builtin, see lecture notes)
len	ALL -> Nat	length of anything
llen	TL -> Nat	length of a true list (not builtin, see lecture notes)
in	ALL x TL -> Bool	(in a X) checks if a is in X (not builtin, see lecture notes)
del	ALL x TL -> TL	(del a X) deletes first occurrence of a from X (not builtin, see lecture notes)

Macros

Name	Description
and	arbitrary # of args, expands to ifs
or	arbitrary # of args, expands to ifs
cond	expand into ifs
+	arbitrary # of args, expands to binary-+
*	arbitrary # of args, expands to binary-*
-	1 (unary--) or 2 (subtraction) args
/	1 (unary-/) or 2 (division) args
<=	less than or equal, expands into <
>	greater than, expands into <
>=	greater than or equal, expands into <
first	synonym for car
rest	synonym for cdr
caar	(car (car ...))
cadr	(car (cdr ...))
c****r	Can have up to 4 a's d's and expands into nested car/cdr's
second	synonym for cadr
third	synonym for caddr, up to tenth supported
list	create a truelist of 0 or more arguments, expands into cons
app	append 0 or more lists, expands into binary-append