-
Notifications
You must be signed in to change notification settings - Fork 629
Pull requests: leanprover/lean4
Author
Label
Projects
Milestones
Reviews
Assignee
Sort
Pull requests list
feat: add BEq instance for ByteArray that uses memcmp
changelog-library
Library
#9549
opened Jul 25, 2025 by
algebraic-dev
Loading…
feat: add A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Iter.toArray lemmas
toolchain-available
#9538
opened Jul 25, 2025 by
pandaman64
Loading…
chore: A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
[match_pattern] should enforce [expose]
toolchain-available
#9534
opened Jul 25, 2025 by
Kha
Loading…
feat: suppress deprecation warnings inside deprecated declarations
toolchain-available
A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#9533
opened Jul 25, 2025 by
jkpjkpjkp
Loading…
feat: generalize Process.output/run to allow an input
changelog-language
Language features, tactics, and metaprograms
toolchain-available
A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#9532
opened Jul 25, 2025 by
kim-em
Loading…
feat: Add This is not necessarily a blocker for merging: but there needs to be a plan
changelog-library
Library
toolchain-available
A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
List.zipWithM and Array.zipWithM
breaks-mathlib
#9528
opened Jul 25, 2025 by
sgraf812
Loading…
feat: elaboration with empty tactic sequences
changelog-language
Language features, tactics, and metaprograms
perf: allow phashmap to specialize
toolchain-available
A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#9519
opened Jul 24, 2025 by
hargoniX
Loading…
feat: add A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
List.mem_finRange
toolchain-available
#9515
opened Jul 24, 2025 by
fgdorais
Loading…
fix: Make Language features, tactics, and metaprograms
mvcgen mintro let/have bindings (#9474)
changelog-language
#9507
opened Jul 24, 2025 by
sgraf812
Loading…
feat: improve CI has verified that Mathlib builds against this PR
changelog-language
Language features, tactics, and metaprograms
toolchain-available
A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
set_option error messages
builds-mathlib
#9496
opened Jul 23, 2025 by
jrr6
Loading…
refactor: update and consolidate attribute-related error messages
breaks-mathlib
This is not necessarily a blocker for merging: but there needs to be a plan
changelog-no
Do not include this PR in the release changelog
toolchain-available
A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
fix: avoid RPC errors in nonexistent identifier hovers
breaks-mathlib
This is not necessarily a blocker for merging: but there needs to be a plan
changelog-pp
Pretty printing
toolchain-available
A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#9494
opened Jul 23, 2025 by
jrr6
Loading…
fix: let simp apply autogenerated congruence theorems
builds-mathlib
CI has verified that Mathlib builds against this PR
changelog-language
Language features, tactics, and metaprograms
toolchain-available
A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#9493
opened Jul 23, 2025 by
kmill
Loading…
feat: have structure instances try synthesizing pending mvars before postponing
builds-mathlib
CI has verified that Mathlib builds against this PR
changelog-language
Language features, tactics, and metaprograms
toolchain-available
A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
feat: allow short config syntax (Language features, tactics, and metaprograms
+opt / -opt) for several parsers
changelog-language
#9437
opened Jul 19, 2025 by
Rob23oba
Loading…
feat: add
popCount using Kernighan's algorithm to the bitblaster
#9416
opened Jul 17, 2025 by
luisacicolini
•
Draft
chore: CI: reactivate Lake cache
toolchain-available
A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
feat: high-level order structures
breaks-mathlib
This is not necessarily a blocker for merging: but there needs to be a plan
changelog-library
Library
toolchain-available
A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Previous Next
ProTip!
Updated in the last three days: updated:>2025-07-22.