## SET-CHECKPOINT-SUMMARY-LIMIT

control printing of key checkpoints upon a proof's failure
Major Section: SWITCHES-PARAMETERS-AND-MODES

See set-gag-mode for a discussion of key checkpoints.

Examples:
; (Default) When a proof fails, print all key checkpoints before
; induction but at most 3 key checkpoints after induction:
(set-checkpoint-summary-limit (nil . 3))

; When a proof fails, print at most 3 key checkpoints before
; induction but all 3 key checkpoints after induction:
(set-checkpoint-summary-limit (3 . nil))

; When a proof fails, print at most 3 key checkpoints before
; induction and at most 5 key checkpoints after induction:
(set-checkpoint-summary-limit (3 . 5))

; When a proof fails, print at most 3 key checkpoints before
; induction and at most 3 key checkpoints after induction:
(set-checkpoint-summary-limit (3 . 3))
; or equivalently,
(set-checkpoint-summary-limit 3)

; When a proof fails, print all key checkpoints:
(set-checkpoint-summary-limit (nil . nil))
; or equivalently,
(set-checkpoint-summary-limit nil)

; When a proof fails, print no information at all about key checkpoints:
(set-checkpoint-summary-limit t)

General Forms:
(set-checkpoint-summary-limit (n1 . n2))
(set-checkpoint-summary-limit n)
(set-checkpoint-summary-limit t)

where each of `n1`

and `n2`

is a natural number or `nil`

. For the
second form, `n`

can be a natural number or `nil`

and is treated as
`(n . n)`

. The value `t`

inhibits all printing of checkpoint summary
information. The values `n1`

and `n2`

determine printing of key
checkpoints generated before the first induction and generated after the
first induction, respectively, where at most `n1`

or `n2`

(respectively)
such key checkpoints are printed unless the value is `nil`

, in which case
there is no limitation.
The argument `x`

for `set-checkpoint-summary-limit`

, as described above,
may be quoted, i.e. supplied as `'x`

or `(quote x)`

. Thus, you may use
the keyword form (see keyword-commands) if you prefer, for example:

:set-checkpoint-summary-limit (nil . 3)