Control printing of key checkpoints upon a proof's failure

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

The argument

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

To see the current limit, invoke

Note that if some subgoal in a set of key checkpoints is