| /-! | |
| # Testing the `pp.deepTerms false` option | |
| Implemented in PR #3201. | |
| -/ | |
| set_option pp.deepTerms false | |
| set_option pp.deepTerms.threshold 8 | |
| /-! | |
| Subterms of terms with depth <= pp.deepTerms.threshold are not omitted | |
| -/ | |
| #check Nat.zero.succ.succ.succ.succ.succ.succ.succ.succ | |
| /-! | |
| Shallow subterms (subterms with depth <= pp.deepTerms.threshold/4) of terms with | |
| depth > pp.deepTerms.threshold are not omitted | |
| -/ | |
| #check Nat.zero.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ | |
| /-! | |
| Deep subterms of terms with depth > pp.deepTerms.threshold are omitted | |
| -/ | |
| #check Nat.zero.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ | |
| /-! | |
| Nothing is omitted in short lists | |
| -/ | |
| #check [1, 2, 3, 4, 5, 6, 7, 8] | |
| /-! | |
| In longer lists, the tail is omitted | |
| -/ | |
| #check [1, 2, 3, 4, 5, 6, 7, 8, 9] | |
| /-! | |
| Checking the message when an omission is copied from the Infoview | |
| -/ | |
| #check [1, 2, 3, 4, 5, 6, 7, 8, ⋯] |