Skip to content

Releases: leanprover/lean4-pr-releases

Release for PR 6214

12 Jan 21:50
Compare
Choose a tag to compare
pr-release-6214

refactor: move registration of namespaces on kernel add into elaborator

Release for PR 5145

12 Jan 21:49
Compare
Choose a tag to compare
pr-release-5145

chore: clean up after update-stage0

Release for PR 6596

11 Jan 00:35
6cce163
Compare
Choose a tag to compare
pr-release-6596

Update script/release_repos.yml

Release for PR 6599

10 Jan 15:27
Compare
Choose a tag to compare
doc: update FFI description

The FFI description didn't mention Int or signed integers.

This PR adds these details.

Release for PR 6598

10 Jan 14:40
Compare
Choose a tag to compare
perf: use C23's `free_sized` when available

This only has an effect on systems with a default allocator where `free_sized` is faster than `free`.

See https://www.open-std.org/jtc1/sc22/wg14/www/docs/n2699.htm for an explanation of this feature.

Co-authored-by: Eric Wieser <[email protected]>

Release for PR 6597

10 Jan 13:59
Compare
Choose a tag to compare
pr-release-6597

fix: trace indentation in info view

Release for PR 6431

10 Jan 23:11
Compare
Choose a tag to compare
pr-release-6431

chore: remove useless lines

Release for PR 6404

10 Jan 14:37
Compare
Choose a tag to compare
pr-release-6404

fix: toNat_ne_iff_ne rename

Release for PR 6402

10 Jan 02:33
75d6f2e
Compare
Choose a tag to compare
pr-release-6402

Update src/Init/Data/BitVec/Lemmas.lean

Release for PR 6306

10 Jan 16:23
Compare
Choose a tag to compare
pr-release-6306

chore: remove sorries