Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
538 commits
Select commit Hold shift + click to select a range
dc8e18c
Merge remote-tracking branch 'origin/main' into bump/v4.29.0
Jan 30, 2026
5829d7b
chore: adaptations for nightly-2026-01-30
Jan 30, 2026
d638107
Merge branch 'bump/nightly-2026-01-30' into nightly-testing
Jan 30, 2026
1e33a08
one adaptation note fixed by main
chenson2018 Jan 30, 2026
cc1df00
chore: adaptations for nightly-2026-01-30
Jan 30, 2026
0af8ac9
Merge branch 'bump/nightly-2026-01-30' into nightly-testing
Jan 30, 2026
2663b63
chore: adaptations for nightly-2026-01-30
Jan 30, 2026
ad76b37
Merge branch 'bump/nightly-2026-01-30' into nightly-testing
Jan 30, 2026
0241271
chore: adaptations for nightly-2026-01-30 (#307)
Jan 30, 2026
e74578e
chore: bump to nightly-2026-01-31 with mathlib at nightly-testing-202…
Jan 31, 2026
c8d97c0
chore: adaptations for nightly-2026-01-31
Jan 31, 2026
f9fa00a
chore: adaptations for nightly-2026-01-31 (#309)
Jan 31, 2026
faac567
Merge main into nightly-testing
Feb 1, 2026
d97ce93
chore: bump to nightly-2026-02-02 with mathlib at nightly-testing-202…
Feb 2, 2026
8782cdf
Merge main into nightly-testing
Feb 3, 2026
44e1e02
Auto-resolved conflicts in lean-toolchain and lake-manifest.json
Feb 3, 2026
3615bb3
chore: adaptations for nightly-2026-02-02
Feb 3, 2026
8b9eb9c
chore: adaptations for nightly-2026-02-02 (#315)
Feb 3, 2026
30af7e5
Merge main into nightly-testing
mathlib-nightly-testing[bot] Feb 4, 2026
d49c166
Merge main into nightly-testing
mathlib-nightly-testing[bot] Feb 4, 2026
a872c17
Merge main into nightly-testing
mathlib-nightly-testing[bot] Feb 6, 2026
a0ac7ff
chore: bump to nightly-2026-02-05 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Feb 6, 2026
db264ae
use Lean.Meta.Instances
chenson2018 Feb 6, 2026
4e3ecf7
simp +instances
chenson2018 Feb 6, 2026
443c31e
simp +instances in CslibTests
chenson2018 Feb 6, 2026
5dd1530
Merge remote-tracking branch 'origin/main' into bump/v4.29.0
Feb 6, 2026
2103c21
chore: adaptations for nightly-2026-02-05
Feb 6, 2026
ab85bff
chore: adaptations for nightly-2026-02-05 (#324)
mathlib-nightly-testing[bot] Feb 6, 2026
0458b6e
Merge main into nightly-testing
mathlib-nightly-testing[bot] Feb 6, 2026
7c79cc4
Merge main into nightly-testing
mathlib-nightly-testing[bot] Feb 7, 2026
ffc0f7a
chore: bump to nightly-2026-02-10 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Feb 10, 2026
d972e98
Auto-resolved conflicts in lean-toolchain and lake-manifest.json
Feb 10, 2026
66107b5
chore: adaptations for nightly-2026-02-10
Feb 10, 2026
15e6b29
chore: adaptations for nightly-2026-02-10 (#330)
mathlib-nightly-testing[bot] Feb 10, 2026
6f161b8
chore: bump to nightly-2026-02-13-rev2 with mathlib at nightly-testin…
mathlib-nightly-testing[bot] Feb 13, 2026
53e1a01
chore: adaptations for nightly-2026-02-13-rev2
Feb 13, 2026
622d921
chore: adaptations for nightly-2026-02-13-rev2 (#332)
mathlib-nightly-testing[bot] Feb 13, 2026
0a02eb1
Merge main into nightly-testing
mathlib-nightly-testing[bot] Feb 14, 2026
e21566e
chore: bump to nightly-2026-02-15-rev1 with mathlib at nightly-testin…
mathlib-nightly-testing[bot] Feb 15, 2026
da945d5
Merge remote-tracking branch 'origin/main' into bump/v4.29.0
Feb 15, 2026
41389cc
chore: adaptations for nightly-2026-02-15-rev1
Feb 15, 2026
f2a87d6
chore: adaptations for nightly-2026-02-15-rev1 (#337)
mathlib-nightly-testing[bot] Feb 15, 2026
da8e43e
Merge main into nightly-testing
mathlib-nightly-testing[bot] Feb 16, 2026
4a56298
chore: bump to nightly-2026-02-16 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Feb 16, 2026
6d00a64
Merge remote-tracking branch 'origin/main' into bump/v4.29.0
Feb 16, 2026
a36a8b0
chore: adaptations for nightly-2026-02-16
Feb 16, 2026
7f01bb9
Merge main into nightly-testing
mathlib-nightly-testing[bot] Feb 16, 2026
636ded9
Merge main into nightly-testing
mathlib-nightly-testing[bot] Feb 17, 2026
4b2015a
Merge main into nightly-testing
mathlib-nightly-testing[bot] Feb 17, 2026
055330f
Merge main into nightly-testing
mathlib-nightly-testing[bot] Feb 17, 2026
b608dc1
Merge main into nightly-testing
mathlib-nightly-testing[bot] Feb 18, 2026
89cd513
Merge main into nightly-testing
mathlib-nightly-testing[bot] Feb 18, 2026
f6e17b7
Merge main into nightly-testing
mathlib-nightly-testing[bot] Feb 19, 2026
b81084a
Merge main into nightly-testing
mathlib-nightly-testing[bot] Feb 19, 2026
efc31a1
set a nightly toolchain
chenson2018 Feb 19, 2026
24e0a5a
manual bump to nightly-2026-02-17
chenson2018 Feb 19, 2026
0e56a9f
Merge remote-tracking branch 'origin/main' into bump/v4.30.0
Feb 19, 2026
4cde412
Merge commit '24e0a5a923e24d374f081a586aa1376ed72630b2' into bump/nig…
Feb 19, 2026
2deedee
chore: adaptations for nightly-2026-02-17
Feb 19, 2026
77ae4f0
Merge main into nightly-testing
mathlib-nightly-testing[bot] Feb 19, 2026
f9ae9ad
Merge main into nightly-testing
mathlib-nightly-testing[bot] Feb 19, 2026
786de85
chore: bump to nightly-2026-02-19 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Feb 19, 2026
a2e9349
use Lean.isImplicitReducible
chenson2018 Feb 19, 2026
424882b
Merge main into nightly-testing
mathlib-nightly-testing[bot] Feb 20, 2026
1b8efc1
Merge main into nightly-testing
mathlib-nightly-testing[bot] Feb 21, 2026
2116efc
chore: bump to nightly-2026-02-21 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Feb 21, 2026
c251390
Merge remote-tracking branch 'origin/main' into bump/v4.30.0
Feb 21, 2026
e7ef5bb
Merge commit '2116efc6f5af698bd719929b3c5258b7e68de549' into bump/nig…
Feb 21, 2026
b4f8a0a
chore: adaptations for nightly-2026-02-21
Feb 21, 2026
f2cc3a0
chore: adaptations for nightly-2026-02-21 (#361)
mathlib-nightly-testing[bot] Feb 21, 2026
e78d20c
Merge main into nightly-testing
mathlib-nightly-testing[bot] Feb 23, 2026
a4559c7
chore: bump to nightly-2026-02-23 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Feb 23, 2026
9a488ca
Merge remote-tracking branch 'origin/main' into bump/v4.30.0
Feb 23, 2026
8994f46
chore: adaptations for nightly-2026-02-23
Feb 23, 2026
af1ca6a
chore: adaptations for nightly-2026-02-23 (#366)
mathlib-nightly-testing[bot] Feb 23, 2026
c98fb7e
chore: bump to nightly-2026-02-23-rev1 with mathlib at nightly-testin…
mathlib-nightly-testing[bot] Feb 24, 2026
d919360
chore: adaptations for nightly-2026-02-23-rev1
Feb 24, 2026
fa542b4
chore: adaptations for nightly-2026-02-23-rev1 (#367)
mathlib-nightly-testing[bot] Feb 24, 2026
e519b45
Merge main into nightly-testing
mathlib-nightly-testing[bot] Feb 24, 2026
e461aa7
Merge main into nightly-testing
mathlib-nightly-testing[bot] Feb 25, 2026
bf84fd6
Merge main into nightly-testing
mathlib-nightly-testing[bot] Feb 25, 2026
3e9dded
chore: bump to nightly-2026-02-25 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Feb 27, 2026
6350a88
adaptation for lean4#12603
chenson2018 Feb 27, 2026
41dd754
Auto-resolved conflicts in lean-toolchain and lake-manifest.json
Feb 27, 2026
216c6fa
chore: adaptations for nightly-2026-02-25
Feb 27, 2026
72c3503
chore: adaptations for nightly-2026-02-25 (#377)
mathlib-nightly-testing[bot] Feb 27, 2026
f6ef535
Merge main into nightly-testing
mathlib-nightly-testing[bot] Feb 27, 2026
2b18ca3
Merge main into nightly-testing
mathlib-nightly-testing[bot] Feb 28, 2026
70f90c0
Merge main into nightly-testing
mathlib-nightly-testing[bot] Mar 2, 2026
6ea7b28
manual bump to 2026-03-02
chenson2018 Mar 3, 2026
ea498e9
Auto-resolved conflicts in lean-toolchain and lake-manifest.json
Mar 3, 2026
28bd035
chore: adaptations for nightly-2026-03-02
Mar 3, 2026
3bac213
chore: adaptations for nightly-2026-03-02 (#395)
mathlib-nightly-testing[bot] Mar 3, 2026
d482a77
Merge main into nightly-testing
mathlib-nightly-testing[bot] Mar 4, 2026
33a2a72
Merge main into nightly-testing
mathlib-nightly-testing[bot] Mar 5, 2026
112445d
Merge main into nightly-testing
mathlib-nightly-testing[bot] Mar 5, 2026
6b920b6
chore: bump to nightly-2026-03-05 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Mar 5, 2026
8608959
Auto-resolved conflicts in lean-toolchain and lake-manifest.json
Mar 5, 2026
ecc3f0f
chore: adaptations for nightly-2026-03-05
Mar 5, 2026
5df7580
chore: adaptations for nightly-2026-03-05 (#402)
mathlib-nightly-testing[bot] Mar 5, 2026
d2c36fc
Merge main into nightly-testing
mathlib-nightly-testing[bot] Mar 5, 2026
231c589
Merge main into nightly-testing
mathlib-nightly-testing[bot] Mar 6, 2026
405ca40
Merge main into nightly-testing
mathlib-nightly-testing[bot] Mar 9, 2026
06a4567
Merge main into nightly-testing
mathlib-nightly-testing[bot] Mar 9, 2026
540c985
Merge main into nightly-testing
mathlib-nightly-testing[bot] Mar 10, 2026
e06c14c
chore: bump to nightly-2026-03-09 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Mar 10, 2026
ab1c7e6
Merge main into nightly-testing
mathlib-nightly-testing[bot] Mar 10, 2026
9888913
Merge main into nightly-testing
mathlib-nightly-testing[bot] Mar 12, 2026
89d5477
Merge main into nightly-testing
mathlib-nightly-testing[bot] Mar 12, 2026
0b924df
Merge main into nightly-testing
mathlib-nightly-testing[bot] Mar 13, 2026
6e74614
manual update to 2026-03-14
chenson2018 Mar 15, 2026
e812068
Auto-resolved conflicts in lean-toolchain and lake-manifest.json
Mar 15, 2026
10a8913
chore: adaptations for nightly-2026-03-14
Mar 15, 2026
8517d04
chore: adaptations for nightly-2026-03-14 (#426)
mathlib-nightly-testing[bot] Mar 15, 2026
bcfd3fb
Merge main into nightly-testing
mathlib-nightly-testing[bot] Mar 17, 2026
e99b770
Merge main into nightly-testing
mathlib-nightly-testing[bot] Mar 17, 2026
942e585
chore: bump to nightly-2026-03-17 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Mar 17, 2026
47c24c7
Merge remote-tracking branch 'origin/main' into bump/v4.30.0
Mar 17, 2026
78d22fe
chore: adaptations for nightly-2026-03-17
Mar 17, 2026
44a0ed0
chore: adaptations for nightly-2026-03-17 (#434)
mathlib-nightly-testing[bot] Mar 17, 2026
6504a8f
Merge main into nightly-testing
mathlib-nightly-testing[bot] Mar 17, 2026
33144c9
Merge main into nightly-testing
mathlib-nightly-testing[bot] Mar 17, 2026
f6a4b5b
chore: bump to nightly-2026-03-18 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Mar 18, 2026
82cebe3
Merge remote-tracking branch 'origin/main' into bump/v4.30.0
Mar 18, 2026
b7d8dc6
chore: adaptations for nightly-2026-03-18
Mar 18, 2026
a7f66bf
chore: adaptations for nightly-2026-03-18 (#441)
mathlib-nightly-testing[bot] Mar 18, 2026
8c9b401
Merge main into nightly-testing
mathlib-nightly-testing[bot] Mar 19, 2026
71272f9
Merge main into nightly-testing
mathlib-nightly-testing[bot] Mar 20, 2026
26bac37
Merge main into nightly-testing
mathlib-nightly-testing[bot] Mar 20, 2026
bf2634f
chore: bump to nightly-2026-03-19 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Mar 20, 2026
275dd22
Merge remote-tracking branch 'origin/main' into bump/v4.30.0
Mar 20, 2026
c5efbb9
chore: adaptations for nightly-2026-03-19
Mar 20, 2026
ecd0cc8
chore: adaptations for nightly-2026-03-19 (#447)
mathlib-nightly-testing[bot] Mar 20, 2026
ef513f8
chore: bump to nightly-2026-03-19-rev1 with mathlib at nightly-testin…
mathlib-nightly-testing[bot] Mar 22, 2026
0cf95b9
getNamespaceSet -> getNamespaces
chenson2018 Mar 22, 2026
71dc8ea
getNamespaceSet -> getNamespaces
chenson2018 Mar 22, 2026
e137a45
chore: adaptations for nightly-2026-03-19-rev1
Mar 22, 2026
b66f914
chore: adaptations for nightly-2026-03-19-rev1 (#451)
mathlib-nightly-testing[bot] Mar 22, 2026
4555ad5
Merge main into nightly-testing
mathlib-nightly-testing[bot] Mar 23, 2026
a704c17
Merge main into nightly-testing
mathlib-nightly-testing[bot] Mar 24, 2026
cd361c8
chore: bump to nightly-2026-03-24 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Mar 24, 2026
d80ead5
Auto-resolved conflicts in lean-toolchain and lake-manifest.json
Mar 24, 2026
af70787
chore: adaptations for nightly-2026-03-24
Mar 24, 2026
e061a6e
chore: adaptations for nightly-2026-03-24 (#454)
mathlib-nightly-testing[bot] Mar 24, 2026
6c4397a
Merge main into nightly-testing
mathlib-nightly-testing[bot] Mar 25, 2026
2121f88
Merge main into nightly-testing
mathlib-nightly-testing[bot] Mar 25, 2026
39738ba
Merge main into nightly-testing
mathlib-nightly-testing[bot] Mar 25, 2026
e23624d
Merge main into nightly-testing
mathlib-nightly-testing[bot] Mar 26, 2026
610a728
Merge main into nightly-testing
mathlib-nightly-testing[bot] Mar 26, 2026
34a1a8c
chore: bump to nightly-2026-03-25 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Mar 26, 2026
d0e81c8
Auto-resolved conflicts in lean-toolchain and lake-manifest.json
Mar 26, 2026
2837a51
chore: adaptations for nightly-2026-03-25
Mar 26, 2026
eded9ac
chore: adaptations for nightly-2026-03-25 (#459)
mathlib-nightly-testing[bot] Mar 26, 2026
ff0c4dd
Merge main into nightly-testing
mathlib-nightly-testing[bot] Mar 30, 2026
fe30057
Merge main into nightly-testing
mathlib-nightly-testing[bot] Mar 31, 2026
ba9b308
chore: bump to nightly-2026-03-31 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Mar 31, 2026
35d6de9
grind failure in nth_of_strictMono (transparency?)
chenson2018 Mar 31, 2026
3df6d03
chore: bump to nightly-2026-04-01 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Apr 1, 2026
ba9a3f0
add an adaptation note
chenson2018 Apr 2, 2026
6936134
grind regression in Proof.expand_onlyAtomicAxioms_dual
chenson2018 Apr 2, 2026
49aa627
segment_range_val grind regressions
chenson2018 Apr 2, 2026
fad1506
map_toCompCfg_left_step grind regression
chenson2018 Apr 2, 2026
4500048
mem_biSup
chenson2018 Apr 2, 2026
c0ace9d
sub_one_mul grind regressions
chenson2018 Apr 2, 2026
ea5ca4e
Merge main into nightly-testing
mathlib-nightly-testing[bot] Apr 2, 2026
e1f0e48
kstar_sub_one grind regression
chenson2018 Apr 2, 2026
a411b73
omegaPow_eq_empty grind regression
chenson2018 Apr 2, 2026
a17ca1b
omegaPow_le_hmul_omegaPow' grind regression
chenson2018 Apr 2, 2026
2d6cdbc
biorth_least_fact
chenson2018 Apr 3, 2026
11bb7a8
tensor_of_par
chenson2018 Apr 3, 2026
7b312aa
bisimilarity_congr_res
chenson2018 Apr 3, 2026
a12780b
Merge main into nightly-testing
mathlib-nightly-testing[bot] Apr 3, 2026
96f0752
omegaPow_coind'
chenson2018 Apr 3, 2026
2bc82dc
remove import from cslib#467 in nightly-testing temporarily
chenson2018 Apr 3, 2026
a5d6b5c
Fix grind failure in NA/toDA.lean
ctchou Apr 3, 2026
72521c2
Fix grind failure in NA/toDA.lean
ctchou Apr 3, 2026
239fd9e
toNAFinAcc_language_eq grind regression
chenson2018 Apr 4, 2026
bcc64c6
toNAFinAcc_language_eq grind regression
chenson2018 Apr 4, 2026
7359770
toNABuchi_language_eq
chenson2018 Apr 4, 2026
024f2e4
congr_language_eq
chenson2018 Apr 5, 2026
0dc60b0
reindex_language_eq
chenson2018 Apr 5, 2026
31204e7
Proof.expand_onlyAtomicAxioms
chenson2018 Apr 5, 2026
4a84152
loop_language_eq
chenson2018 Apr 5, 2026
65f8b27
Fix grind failure in Automata/NA/Sum.lean
ctchou Apr 5, 2026
f1ea3d5
Fix grind failures in Automata/NA/Concat.lean
ctchou Apr 5, 2026
42f89c2
Fix grind failures in Automata/NA/Loop.lean
ctchou Apr 5, 2026
47e76a6
Use Robin Arnez's better proof in NA/Loop.lean
ctchou Apr 6, 2026
42749fe
IsRegular.{compl,zero}
chenson2018 Apr 6, 2026
b484801
finish off RegularLanguage
chenson2018 Apr 6, 2026
7a80f96
buchiCongruence_transfer
chenson2018 Apr 6, 2026
68db938
buchiFamily_cover
chenson2018 Apr 6, 2026
6528578
whitespace
chenson2018 Apr 6, 2026
af786e3
OmegaRegularLanguage
chenson2018 Apr 6, 2026
c8f5e57
grind lint changes
chenson2018 Apr 6, 2026
ff00dd0
Auto-resolved conflicts in lean-toolchain and lake-manifest.json
Apr 6, 2026
2f0c725
chore: adaptations for nightly-2026-04-01
Apr 6, 2026
94eb1aa
Merge main into nightly-testing
mathlib-nightly-testing[bot] Apr 6, 2026
c35990e
Merge main into nightly-testing
mathlib-nightly-testing[bot] Apr 6, 2026
d8cb9bb
Merge main into nightly-testing
mathlib-nightly-testing[bot] Apr 7, 2026
1f82fea
chore: bump to nightly-2026-04-06 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Apr 7, 2026
fd0b4bc
chore: additional module directives from mk_all
chenson2018 Apr 7, 2026
1a7ebec
chore: adaptations for nightly-2026-04-06
Apr 7, 2026
ab632e3
chore: bump to nightly-2026-04-07 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Apr 7, 2026
9a5a077
chore: adaptations for nightly-2026-04-07
Apr 7, 2026
148401b
chore: bump to nightly-2026-04-10 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Apr 10, 2026
8d2f89b
chore: adaptations for nightly-2026-04-10
Apr 10, 2026
0343584
chore: bump to nightly-2026-04-11 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Apr 12, 2026
0078554
chore: adaptations for nightly-2026-04-11
Apr 12, 2026
0592627
Merge main into nightly-testing
mathlib-nightly-testing[bot] Apr 13, 2026
fd66d0a
chore: bump to nightly-2026-04-13 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Apr 13, 2026
a623ea0
chore: adaptations for nightly-2026-04-13
Apr 13, 2026
c8adc6f
Merge main into nightly-testing
mathlib-nightly-testing[bot] Apr 13, 2026
2a0e1ad
Merge main into nightly-testing
mathlib-nightly-testing[bot] Apr 15, 2026
8352f0c
Merge main into nightly-testing
mathlib-nightly-testing[bot] Apr 15, 2026
f545485
chore: bump to nightly-2026-04-16 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Apr 16, 2026
f212c1b
Merge main into nightly-testing
mathlib-nightly-testing[bot] Apr 18, 2026
24a1eb8
chore: adaptations for nightly-2026-04-16
Apr 18, 2026
3ad033e
chore: bump to nightly-2026-04-19 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Apr 19, 2026
5305875
chore: adaptations for nightly-2026-04-19
Apr 19, 2026
806ef25
Merge main into nightly-testing
mathlib-nightly-testing[bot] Apr 19, 2026
ec6166b
Merge main into nightly-testing
mathlib-nightly-testing[bot] Apr 20, 2026
20e44fb
Merge main into nightly-testing
mathlib-nightly-testing[bot] Apr 20, 2026
0e24b20
Merge main into nightly-testing
mathlib-nightly-testing[bot] Apr 21, 2026
557ce04
chore: bump to nightly-2026-04-22 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Apr 22, 2026
71bf357
chore: adaptations for nightly-2026-04-22
Apr 22, 2026
d6368a9
Merge main into nightly-testing
mathlib-nightly-testing[bot] Apr 22, 2026
8bedd14
chore: bump to nightly-2026-04-23 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Apr 23, 2026
31ec1a8
chore: adaptations for nightly-2026-04-23
Apr 23, 2026
29959e5
chore: bump to nightly-2026-04-24 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Apr 24, 2026
0031af2
chore: adaptations for nightly-2026-04-24
Apr 24, 2026
347259c
Merge main into nightly-testing
mathlib-nightly-testing[bot] Apr 24, 2026
ad11211
Merge main into nightly-testing
mathlib-nightly-testing[bot] Apr 25, 2026
4873eac
Merge main into nightly-testing
mathlib-nightly-testing[bot] Apr 25, 2026
1ffd597
chore: bump to nightly-2026-04-25 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Apr 26, 2026
fa21d26
chore: adaptations for nightly-2026-04-25
Apr 26, 2026
61f435a
chore: bump to nightly-2026-04-27 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Apr 27, 2026
99621df
chore: adaptations for nightly-2026-04-27
Apr 27, 2026
71d53d5
Merge main into nightly-testing
mathlib-nightly-testing[bot] Apr 27, 2026
13b89cf
Merge main into nightly-testing
mathlib-nightly-testing[bot] Apr 29, 2026
f96d2c2
Merge main into nightly-testing
mathlib-nightly-testing[bot] Apr 30, 2026
06996b1
Merge main into nightly-testing
mathlib-nightly-testing[bot] Apr 30, 2026
4a08821
Merge main into nightly-testing
mathlib-nightly-testing[bot] May 2, 2026
1505b64
Merge main into nightly-testing
mathlib-nightly-testing[bot] May 3, 2026
f530fc0
chore: bump to nightly-2026-05-03 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] May 3, 2026
26dee6f
Fix failure in Cslib/Computability/Automata/NA/Concat.lean
ctchou May 3, 2026
130fb84
Fix failure in Cslib/Computability/Languages/Congruences/BuchiCongrue…
ctchou May 3, 2026
9de72b7
Typing.progress
chenson2018 May 3, 2026
5a7f08f
chore: adaptations for nightly-2026-05-03
chenson2018 May 3, 2026
8798001
chore: bump to nightly-2026-05-04 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] May 4, 2026
f88ab11
chore: adaptations for nightly-2026-05-04
May 4, 2026
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions lake-manifest.json
Original file line number Diff line number Diff line change
Expand Up @@ -5,10 +5,10 @@
"type": "git",
"subDir": null,
"scope": "",
"rev": "09f28100a1eedd6f03d1ef4c36aafb9762ee9f1d",
"rev": "516318b4c53a12c6db4c506b8aba14bed1239b1c",
"name": "mathlib",
"manifestFile": "lake-manifest.json",
"inputRev": "nightly-testing-2026-05-03",
"inputRev": "nightly-testing-2026-05-04",
"inherited": false,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover-community/plausible",
Expand Down Expand Up @@ -75,7 +75,7 @@
"type": "git",
"subDir": null,
"scope": "leanprover-community",
"rev": "953e9065fe10a846da3b85497f278311796738e2",
"rev": "a5057d09bbda63aed64ee5b88d37b63da3e46a09",
"name": "batteries",
"manifestFile": "lake-manifest.json",
"inputRev": "nightly-testing",
Expand Down
2 changes: 1 addition & 1 deletion lakefile.toml
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ weak.linter.unicodeLinter = false
[[require]]
name = "mathlib"
git = "https://github.com/leanprover-community/mathlib4-nightly-testing"
rev = "nightly-testing-2026-05-03"
rev = "nightly-testing-2026-05-04"

[[lean_lib]]
name = "Cslib"
Expand Down
2 changes: 1 addition & 1 deletion lean-toolchain
Original file line number Diff line number Diff line change
@@ -1 +1 @@
leanprover/lean4:nightly-2026-05-03
leanprover/lean4:nightly-2026-05-04
Loading