chapter 3

:redef

guard checking

(set-guard-checking :none)

(set-guard-checking :all)

:doc set-guard-checking

:DOC GUARD-EVALUATION-TABLE

trace

:doc trace

(trace$ pascal)

(untrace$ pascal)

declarations

(declare (ignore v1 … vn))

to indicate variables are unused in body

(declare (xargs :guard g))

to declare that the gard for a defined function or macro is the expression g

(declare (xargs :measure m)

to declare the “measure” to be used to prove termination