SET-CHECKPOINT-SUMMARY-LIMIT

control printing of key checkpoints upon a proof's failure
Major Section:  OTHER

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

where each of 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.