[#14519] 9077, with options, downstream - #10

Closed

downstream-lean4[bot] wants to merge 11 commits into

adaptation-14519

Commits on Jul 23, 2026

downstream: follow upstream PR
downstream-lean4[bot]
committed
c434240
Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/14248

leanprover-community-mathlib4-bot
authored and
datokrat
committed
45d7905

Commits on Jul 27, 2026

cleanups, more analysis
datokrat
committed
82412cd

Commits on Jul 29, 2026

get rid of some backward options, also relying on appOnFailure false
datokrat
committed
df28b26
hmm, breaks
datokrat
committed
4e64af9
fixes
datokrat
committed
17b0aee

Commits on Jul 30, 2026

downstream: follow upstream PR
downstream-lean4[bot]
committed
52a9dea

Commits on Jul 31, 2026