36c2511b27
Gives more control over pretty printing metavariables. - When `pp.mvars.levels` is false, then universe level metavariables pretty print as `_` rather than `?u.22` - When `pp.mvars.anonymous` is false, then anonymous metavariables pretty print as `?_` rather than `?m.22`. Named metavariables still pretty print with their names. When this is false, it also sets `pp.mvars.levels` to false, since every level metavariable is anonymous. - When `pp.mvars` is false, then all metavariables pretty print as `?_` or `_`. Modifies TryThis to use `pp.mvars.anonymous` rather than doing a post-delaboration modification. This incidentally improves TryThis since it now prints universe level metavariables as `_` rather than `?u.22`. |
||
|---|---|---|
| .. | ||
| Basic.lean | ||
| Diff.lean | ||
| InteractiveCode.lean | ||
| InteractiveDiagnostic.lean | ||
| InteractiveGoal.lean | ||
| TaggedText.lean | ||
| Types.lean | ||
| UserWidget.lean | ||