ACL2s reference

Types

Name	Recognizer	Description
all	allp	the ACL2s universe
atom	atom	atomic data: numbers, strings, symbols, characters, ...
symbol	symbolp	symbols
boolean	booleanp	t or nil
bool	boolp	alias for boolean
rational	rationalp	rational numbers (we make the simplifying assumption (which is not true) that all numbers are rationals)
integer	integerp	integers
int	intp	alias for integer
nat	natp	natural numbers (integers >= 0)
pos	posp	integers > 0
neg	negp	integers < 0
non-pos-integer	non-pos-integerp	integers <= 0
non-0-integer	non-0-integerp	integers \ {0}
non-neg-rational	non-neg-rationalp	rationals >= 0
pos-rational	pos-rationalp	rationals > 0
neg-rational	neg-rationalp	rationals < 0
non-pos-rational	non-pos-rationalp	rationals <= 0
non-0-rational	non-0-rationalp	rationals \ {0}
cons	consp	conses, constructed with cons
true-list	true-listp	true lists (nil terminated cons)
tl	tlp	alias for true-list
list	listp	conses or nil
non-empty-true-list	non-empty-true-listp	non-empty true-list
ne-tl	ne-tlp	alias for non-empty-true-list
alist	alistp	Association list: list of conses
var	varp	Non-constant, variable-like symbols

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
not	All -> Bool	(not x) = (if x nil t)
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)
=	Rational x Rational -> Bool	checks if args are equal
/=	Rational x Rational -> Bool	checks if args differ
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 /
min	Rational x Rational -> Rational	minimum
max	Rational x Rational -> Rational	maximum
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
zp	Nat -> Bool	is the number = 0?
zip	Int -> Bool	is the number = 0?
zerop	Rational -> Bool	is the number = 0?
evenp	Integer -> Bool	is the number even?
oddp	Integer -> Bool	is the number odd?
endp	List -> Bool	is the list empty?
lendp	TL -> Bool	is the TL empty?
cons	All x All -> Cons	create a cons
lcons	All x TL -> NE-TL	create a NE-TL
car	List -> All	car of a list, (car nil)=nil
cdr	List -> All	cdr of a list, (cdr nil)=nil
left	Cons -> All	car of a cons
right	Cons -> All	cdr of a cons
head	NE-TL -> All	car of a ne-tl
tail	NE-TL -> TL	cdr of a ne-tl
acons	All x All x Alist -> Alist	Add a cons to an alist
snoc	TL x All -> TL	Add object to end of a TL
nth	Nat x TL -> All	nth element; nil if nat too large
nthcdr	Nat x TL -> All	nth cdr of a TL
update-nth	Nat x All x TL -> TL	Update nth element of a TL
binary-append	TL x All -> All	concatenation
bin-app	TL x TL -> TL	concatenation
rev	ALL -> TL	reverse
lrev	TL -> TL	reverse a list
len	ALL -> Nat	length of anything
llen	TL -> Nat	length of a true list
in	ALL x TL -> Bool	(in a X) checks if a is in X
nin	ALL x TL -> Bool	(not (in a X))
del	ALL x TL -> TL	(del a X) deletes first occurrence of a from X (not builtin, see lecture notes)
cons-size	ALL -> Nat	returns the "size" of its input (see lecture notes)

Macros

Name	Description
==	abbreviation for equal
!=	abbreviation for (not (equal ...))
!	abbreviation for (not ...)
=>	abbreviation for implies
and	arbitrary # of args, expands into ifs
^	abbreviation for and
or	arbitrary # of args, expands into ifs
v	abbreviaton for or
cond	expand into ifs
+	arbitrary # of args, expands to binary-+
1+	expands to (+ 1 ...)
*	arbitrary # of args, expands to binary-*
-	1 (unary--) or 2 (subtraction) args
1-	expands to (- ... 1)
/	1 (unary-/) or 2 (division) args
<=	less than or equal, expands into <
>	greater than, expands into <
>=	greater than or equal, expands into <
caar	(car (car ...))
cadr	(car (cdr ...))
c****r	Can have up to 4 a's d's and expands into nested cars/cdrs
first	synonym for car
second	synonym for cadr
third	synonym for caddr, up to tenth supported
rest	synonym for cdr
lcar	synonym for head
lcdr	synonym for tail
lcaar	(lcar (lcar ...))
lcadr	(lcar (lcdr ...))
lc****r	Can have up to 4 a's d's and expands into nested lcars/lcdrs
lfirst	synonym for lcar
lsecond	synonym for lcadr
lthird	synonym for lcaddr, up to ltenth supported
list	create a truelist of 0 or more arguments, expands into cons
append	append 0 or more lists, expands into binary-append
app	append 0 or more lists, expands into bin-app
match	provided pattern-matching capabilities