e29d75a961
By having the `pp.proofs` feature use `⋯` when omitting proofs, when users copy/paste terms from the InfoView the elaborator can give an error message explaining why the term cannot be elaborated. Also adds `pp.proofs.threshold` option to allow users to pretty print shallow proof terms. By default, only atomic proof terms are pretty printed. This adjustment was suggested in PR #3201, which added `⋯` and the related `pp.deepTerms` option. |
||
|---|---|---|
| .. | ||
| Delaborator | ||
| Basic.lean | ||
| Delaborator.lean | ||
| Formatter.lean | ||
| Parenthesizer.lean | ||