Repository navigation

feat: `Backreporter`s - #170

Draft

thorimur wants to merge 20 commits into

leanprover-community:mainfrom

thorimur:backreporters

Commits on Oct 2, 2026

feat: backreporters
thorimur
committed
68ebf55
feat: `#min_imports`
thorimur
committed
62df830
chore: dedent
thorimur
committed
34b4cb0
chore: docs
thorimur
committed
308575e
test: minimports
thorimur
committed
934df9b
chore: modifications
thorimur
committed
fd84bec
chore: root
thorimur
committed
c29e910
chore: tweaks
thorimur
committed
fa538c2
chore: tweak
thorimur
committed
143a074
chore: chores
thorimur
committed
c5e66d2
chore: meta warning
thorimur
committed
c08e784
chore: docs, ignore `#min_imports` import
thorimur
committed
5157ac8
chore: cleanup
thorimur
committed
dbb5373
chore: fix tests
thorimur
committed
b36acbe
chore: unrelated warning?
thorimur
committed
49f03a8
Merge branch 'main' into min-imports-module
thorimur
committed
d10f290
chore: restrict PR to backreporters
thorimur
committed
9f90de2
chore: oops, TODOs
thorimur
committed
c57b74c

Commits on Oct 4, 2026

chore: missing copyright header
thorimur
committed
12e2866

Commits on Oct 5, 2026

chore: `runLinterLikes` refactor
thorimur
committed
85f35df