L

lean

Settings | Report Duplicate

0

I Use This!

Very High Activity

Commits : Listings

Analyzed about 15 hours ago. based on code collected about 16 hours ago.

Commit Message	Contributor	Files Modified	Lines Added	Lines Removed	Code Location	Date
Sep 24, 2025 — Oct 24, 2025 Showing page 4 of 10 Search / Filter on:
chore: CI: overhaul check level logic (#10806)	Sebastian Ullrich	More...				9 days ago
chore: lean.code-workspace: fix terminal cwd (#10802)	Sebastian Ullrich	More...				9 days ago
feat: compress generated `grind` tactic sequences using `<;>` (#10808)	Leonardo de Moura	More...				9 days ago
feat: add `splitNext` `grind` action (#10801)	Leonardo de Moura	More...				9 days ago
fix: consider underscores in `getHexNumSize` (#10719)	Rob23oba	More...				9 days ago
chore: remove test for #10766 (#10804)	nomeata as Joachim Breitner	More...				9 days ago
feat: redefine HashSet.union and add lemmas (#10611)	Wojciech Różowski	More...				9 days ago
fix: only run `processInaccessibleAsCtor` if there is at least one constructor around (#10793)	nomeata as Joachim Breitner	More...				9 days ago
chore: add .vscode/settings.json to .gitignore (#10795)	Marc Huisinga	More...				9 days ago
chore: make `extCore` and `customEliminators` public for Batteries (#10799)	Kim Morrison	More...				9 days ago
chore: remove bad grind _=_ annotation on List.contains_iff_mem (#10800)	Kim Morrison	More...				9 days ago
feat: `intro` and `assertAll` as actions (#10798)	Leonardo de Moura	More...				10 days ago
fix: unknown identifier minimization (#10797)	Marc Huisinga	More...				10 days ago
feat: lazy message with `grind` state (#10791)	Leonardo de Moura	More...				10 days ago
chore: even more module system fixes and refinements from Mathlib porting (#10726)	Sebastian Ullrich	More...				10 days ago
fix: preserve error locations when expanding match arms (#10783)	nomeata as Joachim Breitner	More...				10 days ago
chore: CI: re-enable mistakenly deactivated tests for Linux Lake (#10788)	Sebastian Ullrich	More...				10 days ago
fix: detect private references in inferred type of public def (#10762)	Sebastian Ullrich	More...				10 days ago
refactor: processLeaf: Only look at first alt (#10774)	nomeata as Joachim Breitner	More...				10 days ago
fix: hovers and docstrings for (co)inductive types (#10738)	David Thrane Christiansen	More...				10 days ago
feat: implement `mvcgen?`, expanding to `mvcgen invariants?` (#10782)	Sebastian Graf	More...				10 days ago
fix: improve error message when `decide +kernel` fails (#10780)	nomeata as Joachim Breitner	More...				10 days ago
feat: hover information for `grind` anchors (#10779)	Leonardo de Moura	More...				11 days ago
feat: hygiene for `grind` interactive mode (#10778)	Leonardo de Moura	More...				11 days ago
feat: improvements to release automation (#10777)	Kim Morrison	More...				11 days ago
feat: hash map iterators (#10761)	Paul Reichert	More...				11 days ago
feat: `flatMap` iterator combinator (#10728)	Paul Reichert	More...				11 days ago
chore: demote Intel macOS to Tier 2 platform (#10770)	Sebastian Ullrich	More...				11 days ago
refactor: use `Shrink` stub in the iterator framework (#10725)	Paul Reichert	More...				11 days ago
chore: update stage0	Lean stage0 autoupdater	More...				11 days ago

←
1
2
3
4
5
6
7
8
9
10
→