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.