Major Section: OTHER

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

Examples:where each of; (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) state)

; 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) state)

; 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) state)

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

General Forms: (set-checkpoint-summary-limit '(n1 . n2) state) (set-checkpoint-summary-limit nil state)

`n1`

and `n2`

is a natural number or `nil`

. For the
second form, `nil`

is treated as `'(nil . nil)`

. 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.