-
Notifications
You must be signed in to change notification settings - Fork 668
Pull requests: leanprover/lean4
Author
Label
Projects
Milestones
Reviews
Assignee
Sort
Pull requests list
chore: A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
CommandElabM.liftCoreM should not reset InfoState.lazyAssignment
toolchain-available
fix: expose instance implementation functions
changelog-language
Language features and metaprograms
toolchain-available
A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#10517
opened Sep 23, 2025 by
nomeata
Loading…
feat: new String.Slice API
toolchain-available
A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
feat: helper functions for premise selection API
changelog-language
Language features and metaprograms
feat: add Library
toolchain-available
A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Std.CancellationToken type
changelog-library
#10510
opened Sep 22, 2025 by
algebraic-dev
Loading…
feat: expand logic to determine local time
changelog-library
Library
toolchain-available
A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#10509
opened Sep 22, 2025 by
sertonix
Loading…
fix: .congr_simp for non-defs
builds-mathlib
CI has verified that Mathlib builds against this PR
changelog-language
Language features and metaprograms
toolchain-available
A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#10508
opened Sep 22, 2025 by
nomeata
Loading…
chore: update bench/riskv-ast.lean
toolchain-available
A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
chore: add test for #10469 regression
builds-mathlib
CI has verified that Mathlib builds against this PR
toolchain-available
A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#10497
opened Sep 22, 2025 by
kim-em
Loading…
chore: minor module system fixes from batteries port
breaks-mathlib
This is not necessarily a blocker for merging: but there needs to be a plan
toolchain-available
A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#10496
opened Sep 22, 2025 by
Kha
Loading…
feat: improve error messages for ambiguous CI has verified that Mathlib builds against this PR
toolchain-available
A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
3.toDecmial syntax
builds-mathlib
#10488
opened Sep 21, 2025 by
robsimmons
Loading…
feat: adds a simple Library
toolchain-available
A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Http library to Std
changelog-library
#10478
opened Sep 20, 2025 by
algebraic-dev
Loading…
refactor: lake: introduce CI has verified that Mathlib builds against this PR
changelog-lake
Lake
toolchain-available
A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
LogConfig
builds-mathlib
#10468
opened Sep 20, 2025 by
tydeu
Loading…
chore: make Waiting for someone to review the PR
toolchain-available
A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Subrelation reducible
awaiting-review
#10464
opened Sep 19, 2025 by
fgdorais
Loading…
feat: A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
scripts/Modulize.lean, and subsequent batteries fixes
toolchain-available
feat: redefine Library
toolchain-available
A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
String, part two
changelog-library
#10457
opened Sep 19, 2025 by
TwoFX
Loading…
feat: lake: rename dependencies
builds-mathlib
CI has verified that Mathlib builds against this PR
changelog-lake
Lake
toolchain-available
A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#10452
opened Sep 19, 2025 by
tydeu
Loading…
feat: grind linarith synthesis issues explain changes in behaviour
changelog-tactics
User facing tactics
#10448
opened Sep 19, 2025 by
kim-em
Loading…
feat: unknown identifier code actions for auto-implicits
builds-mathlib
CI has verified that Mathlib builds against this PR
changelog-server
Language server, widgets, and IDE extensions
toolchain-available
A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#10442
opened Sep 18, 2025 by
mhuisi
Loading…
chore: remove unhelpful grind annotations
toolchain-available
A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#10435
opened Sep 18, 2025 by
kim-em
Loading…
fix: use Language features and metaprograms
toolchain-available
A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
realizeGlobalConstNoOverloadWithInfo for grind_pattern elaboration
changelog-language
#10427
opened Sep 17, 2025 by
Rob23oba
Loading…
chore: improve docstring of pipe operators
toolchain-available
A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#10413
opened Sep 16, 2025 by
jcreedcmu
Loading…
Previous Next
ProTip!
Follow long discussions with comments:>50.