lean4-htt/src/Lean/Widget
Sebastian Ullrich dda88c9926
feat: infoview.maxTraceChildren (#3370)
Incrementally unveil trace children for excessively large nodes to
improve infoview rendering time, adjust particularly chatty
`simp.ground` trace to make use of it.
2024-02-17 14:04:46 +00:00
..
Basic.lean feat: bundle of widget improvements (#2964) 2023-12-21 06:24:33 +00:00
Diff.lean feat: add context and term data to goals 2023-01-13 17:13:02 -08:00
InteractiveCode.lean feat: have pp.proofs use for omission (#3241) 2024-02-15 21:49:41 +00:00
InteractiveDiagnostic.lean feat: infoview.maxTraceChildren (#3370) 2024-02-17 14:04:46 +00:00
InteractiveGoal.lean feat: partial context info (#3159) 2024-01-22 12:34:20 +00:00
TaggedText.lean chore: use new comment syntax 2022-09-14 08:26:17 -07:00
Types.lean feat: bundle of widget improvements (#2964) 2023-12-21 06:24:33 +00:00
UserWidget.lean feat: add [builtin_widget_module] (#3288) 2024-02-09 11:20:46 +00:00