Zulip Chat Archive
Stream: lean4
Topic: better formatting for `diagnostics` output
Matthew Ballard (Aug 03 2024 at 11:45):
lean#4897 makes the current output go from
info: [reduction] unfolded declarations (max: 1725, num: 4): ▼
Nat.rec ↦ 1725
Eq.rec ↦ 1114
Acc.rec ↦ 1050
PSigma.rec ↦ 513[reduction] unfolded reducible declarations (max: 1577, num: 3): ▼
Nat.casesOn ↦ 1577
Eq.ndrec ↦ 984
PSigma.casesOn ↦ 513[kernel] unfolded declarations (max: 1193, num: 5): ▼
Nat.casesOn ↦ 1193
Nat.rec ↦ 1065
Eq.ndrec ↦ 973
Eq.rec ↦ 973
Acc.rec ↦ 754use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
to
info: [reduction] unfolded declarations (max: 1725, num: 4): ▼
[] Nat.rec ↦ 1725
[] Eq.rec ↦ 1114
[] Acc.rec ↦ 1050
[] PSigma.rec ↦ 513
[reduction] unfolded reducible declarations (max: 1577, num: 3): ▼
[] Nat.casesOn ↦ 1577
[] Eq.ndrec ↦ 984
[] PSigma.casesOn ↦ 513
[kernel] unfolded declarations (max: 1193, num: 5): ▼
[] Nat.casesOn ↦ 1193
[] Nat.rec ↦ 1065
[] Eq.ndrec ↦ 973
[] Eq.rec ↦ 973
[] Acc.rec ↦ 754
use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
when unfolding children in the infoview.
Per the guidelines, it is currently a draft because it has not any blessing from a developer yet.
Last updated: May 02 2025 at 03:31 UTC