L

lean

Settings | Report Duplicate

0

I Use This!

Very High Activity

Commits : Listings

Analyzed about 19 hours ago. based on code collected 1 day ago.

Commit Message	Contributor	Files Modified	Lines Added	Lines Removed	Code Location	Date
Oct 12, 2025 — Oct 12, 2026 Showing page 1 of 1,386 Search / Filter on:
fix: normalize `BitVec.ofNat w k` literals with symbolic width in `grind` new normalizer (#15624)	Leonardo de Moura	More...				2 days ago
feat: simplify propositional binder domains in `Sym.simp` (#15623)	Leonardo de Moura	More...				2 days ago
fix: drop metadata on the arithmetic spine in the `Sym.Arith` normalizer (#15619)	Leonardo de Moura	More...				2 days ago
fix: canonicalize class fields that are not global instances in `Sym.canon` (#15618)	Leonardo de Moura	More...				2 days ago
feat: add a few more BitVec terms to bv_decide (#15616)	Henrik Böving	More...				2 days ago
fix: keep a `Prop` hypothesis when `grind` applies eager `cases` to it (#15612)	Leonardo de Moura	More...				3 days ago
fix: generate a script for every goal in `grind?` when parameters split the goal (#15611)	Leonardo de Moura	More...				3 days ago
feat: assert non-indexable ground theorems as facts in `grind` parameters (#15609)	Leonardo de Moura	More...				3 days ago
fix: validate `finish?` suggestions at the goal before its parameters are asserted (#15606)	Leonardo de Moura	More...				3 days ago
fix: preserve `inj` and `funCC` parameters in `grind?` and `finish?` suggestions (#15602)	Leonardo de Moura	More...				3 days ago
fix: compare instances at `.implicit` transparency in `isDefEqI` (#15600)	Leonardo de Moura	More...				3 days ago
fix: queue solver callbacks replayed during `grind` internalization (#15599)	Leonardo de Moura	More...				3 days ago
refactor: share error and promise helpers in the libuv bindings (#15594)	Sofia Rodrigues	More...				3 days ago
refactor: add RAII-based scoped lock guard (#15547)	Sofia Rodrigues	More...				3 days ago
refactor: embed libuv handles in the uv socket, timer and signal objects (#15545)	Sofia Rodrigues	More...				3 days ago
chore: lake: clear IR artifacts before `leanir` (#15570)	Mac Malone	More...				4 days ago
fix: missing zero check when propagating implied equalities in `grind ring` (#15589)	Leonardo de Moura	More...				4 days ago
fix: builtin component instances in the `grind` canonicalizer (#15588)	Leonardo de Moura	More...				4 days ago
fix: reuse the goal's WP instance when building vcgen spec rules (#15555)	Sebastian Graf	More...				4 days ago
fix: evaluate `cond` lazily in `cbv` (#15582)	Sebastian Graf	More...				4 days ago
feat: guard WP.Frames by the ambient precondition (#15497)	Sebastian Graf	More...				4 days ago
chore: rebalance `libleanshared` DLL split on Windows to avoid symbol limit (#15573)	Sebastian Ullrich	More...				4 days ago
refactor: clarify name and meaning of `LEAN_MAX_CTOR_FIELDS` (#15536)	Sebastian Ullrich	More...				4 days ago
fix: make the export file reader more robust (#15542)	nomeata as Joachim Breitner	More...				4 days ago
perf: record the original kind of an async theorem on the main thread (#15575)	Sebastian Ullrich	More...				4 days ago
chore: code action to add the deprecation date (#15572)	Julia Markus Himmel	More...				4 days ago
fix: handling of 0 in JsonNumber.lt (#15571)	Wojciech Nawrocki	More...				4 days ago
chore: remove leftovers of the old code generator from `Environment` (#15561)	Sebastian Ullrich	More...				4 days ago
fix: do not export `MapDeclarationExtension` entries of private declarations (#15558)	Sebastian Ullrich	More...				4 days ago
fix: do not export realizations triggered only from proofs (#15559)	Sebastian Ullrich	More...				4 days ago

←
1
2
3
4
5
6
7
8
9
…
1385
1386
→