max_print_depth
Globals.max_print_depth : int ref
Sets depth bound on prettyprinting.
The reference variable max_print_depth is used to define the maximum
depth of printing for the pretty printer. If the number of blocks (an
internal notion used by the prettyprinter) becomes greater than the
value set by max_print_depth then the blocks are abbreviated by the
holophrast .... By default, the value of max_print_depth is ~1.
This is interpreted to mean 'print everything'.
Failure
Never fails.
Example
To change the maximum depth setting to 10, the command will be:
- max_print_depth := 10;
> val it = () : unit
The theorem numeralTheory.numeral_distrib then prints as follows:
> numeralTheory.numeral_distrib;
val it =
⊢ (∀n. 0 + n = n) ∧ (∀n. n + 0 = n) ∧
(∀n m. NUMERAL n + NUMERAL m = NUMERAL (numeral$iZ (n + m))) ∧
(∀n. 0 * n = 0) ∧ (∀n. n * 0 = 0) ∧
(∀n m. NUMERAL n * NUMERAL m = NUMERAL (n * m)) ∧ (∀n. 0 − n = 0) ∧
(∀n. n − 0 = n) ∧ (∀n m. NUMERAL n − NUMERAL m = NUMERAL (n − m)) ∧
(∀n. 0 ** NUMERAL (BIT1 n) = 0) ∧ (∀n. 0 ** NUMERAL (BIT2 n) = 0) ∧
(∀n. n ** 0 = 1) ∧ (∀n m. NUMERAL n ** NUMERAL m = NUMERAL (n ** m)) ∧
SUC 0 = 1 ∧ (∀n. SUC (NUMERAL n) = NUMERAL (SUC n)) ∧ PRE 0 = 0 ∧
(∀n. PRE (NUMERAL n) = NUMERAL (PRE n)) ∧
(∀n. NUMERAL n = 0 ⇔ n = ZERO) ∧ (∀n. 0 = NUMERAL n ⇔ n = ZERO) ∧
(∀n m. NUMERAL n = NUMERAL m ⇔ n = m) ∧ (∀n. n < 0 ⇔ F) ∧
(∀n. 0 < NUMERAL n ⇔ ZERO < n) ∧ (∀n m. NUMERAL n < NUMERAL m ⇔ n < m) ∧
(∀n. 0 > n ⇔ F) ∧ (∀n. NUMERAL n > 0 ⇔ ZERO < n) ∧
(∀n m. NUMERAL n > NUMERAL m ⇔ m < n) ∧ (∀n. 0 ≤ n ⇔ T) ∧
(∀n. NUMERAL n ≤ 0 ⇔ n ≤ ZERO) ∧ (∀n m. NUMERAL n ≤ NUMERAL m ⇔ n ≤ m) ∧
(∀n. n ≥ 0 ⇔ T) ∧ (∀n. 0 ≥ n ⇔ n = 0) ∧
(∀n m. NUMERAL n ≥ NUMERAL m ⇔ m ≤ n) ∧ (∀n. ODD (NUMERAL n) ⇔ ODD n) ∧
(∀n. EVEN (NUMERAL n) ⇔ EVEN n) ∧ ¬ODD 0 ∧ EVEN 0: thm