Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
703 commits
Select commit Hold shift + click to select a range
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
0b01373
chore: update lean-toolchain to leanprover/lean4:nightly-2026-04-06
kim-em Apr 7, 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
d7a5214
Merge remote-tracking branch 'origin/main' into bump/v4.31.0
Apr 7, 2026
1a7ebec
chore: adaptations for nightly-2026-04-06
Apr 7, 2026
42d0b00
chore: adaptations for nightly-2026-04-06 (#474)
mathlib-nightly-testing[bot] 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
7e958de
chore: adaptations for nightly-2026-04-07 (#476)
mathlib-nightly-testing[bot] 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
0cd9abb
chore: adaptations for nightly-2026-04-10 (#484)
mathlib-nightly-testing[bot] 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
2f4e427
chore: adaptations for nightly-2026-04-11 (#487)
mathlib-nightly-testing[bot] 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
2b96717
Auto-resolved conflicts in lean-toolchain and lake-manifest.json
Apr 13, 2026
a623ea0
chore: adaptations for nightly-2026-04-13
Apr 13, 2026
0dded92
chore: adaptations for nightly-2026-04-13 (#489)
mathlib-nightly-testing[bot] 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
04ca8d8
Auto-resolved conflicts in lean-toolchain and lake-manifest.json
Apr 18, 2026
24a1eb8
chore: adaptations for nightly-2026-04-16
Apr 18, 2026
298a9f7
chore: adaptations for nightly-2026-04-16 (#498)
mathlib-nightly-testing[bot] 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
2a6377c
chore: adaptations for nightly-2026-04-19 (#500)
mathlib-nightly-testing[bot] 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
7b76f25
Merge remote-tracking branch 'origin/main' into bump/v4.31.0
Apr 22, 2026
71bf357
chore: adaptations for nightly-2026-04-22
Apr 22, 2026
6c753af
chore: adaptations for nightly-2026-04-22 (#513)
mathlib-nightly-testing[bot] 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
5644bea
Merge remote-tracking branch 'origin/main' into bump/v4.31.0
Apr 23, 2026
31ec1a8
chore: adaptations for nightly-2026-04-23
Apr 23, 2026
ac752be
chore: adaptations for nightly-2026-04-23 (#515)
mathlib-nightly-testing[bot] 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
5bc1cf1
chore: adaptations for nightly-2026-04-24 (#519)
mathlib-nightly-testing[bot] 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
fcd9911
Merge remote-tracking branch 'origin/main' into bump/v4.31.0
Apr 26, 2026
fa21d26
chore: adaptations for nightly-2026-04-25
Apr 26, 2026
d7f4709
chore: adaptations for nightly-2026-04-25 (#520)
mathlib-nightly-testing[bot] 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
df8755f
chore: adaptations for nightly-2026-04-27 (#521)
mathlib-nightly-testing[bot] 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
b528f5d
lakefile conflict
chenson2018 May 3, 2026
5a7f08f
chore: adaptations for nightly-2026-05-03
chenson2018 May 3, 2026
bf5282a
chore: adaptations for nightly-2026-05-03 (#541)
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
9f71b96
chore: adaptations for nightly-2026-05-04 (#543)
mathlib-nightly-testing[bot] May 4, 2026
45d50d0
Merge main into nightly-testing
mathlib-nightly-testing[bot] May 5, 2026
511c033
Merge main into nightly-testing
mathlib-nightly-testing[bot] May 6, 2026
05a4b75
chore: bump to nightly-2026-05-05 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] May 6, 2026
fcb6037
chore: bump to nightly-2026-05-06 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] May 6, 2026
64e20e1
conflict
chenson2018 May 6, 2026
d29be92
chore: adaptations for nightly-2026-05-06
chenson2018 May 6, 2026
8ea247a
chore: adaptations for nightly-2026-05-06 (#551)
chenson2018 May 6, 2026
1101c9f
Merge main into nightly-testing
mathlib-nightly-testing[bot] May 6, 2026
75ea8b9
Merge main into nightly-testing
mathlib-nightly-testing[bot] May 7, 2026
e181043
fix: remove simp from modal logic definitions
fmontesi May 8, 2026
ff154d2
chore: bump to nightly-2026-05-07 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] May 8, 2026
d5ae2e3
Merge remote-tracking branch 'origin/main' into bump/v4.31.0
May 8, 2026
78df461
chore: adaptations for nightly-2026-05-07
May 8, 2026
23d0599
chore: adaptations for nightly-2026-05-07 (#555)
mathlib-nightly-testing[bot] May 8, 2026
ac0df66
chore: bump to nightly-2026-05-10 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] May 11, 2026
6423f37
chore: adaptations for nightly-2026-05-10
May 11, 2026
1190e93
chore: adaptations for nightly-2026-05-10 (#559)
mathlib-nightly-testing[bot] May 11, 2026
350f5a9
Merge main into nightly-testing
mathlib-nightly-testing[bot] May 11, 2026
1b21992
Merge main into nightly-testing
mathlib-nightly-testing[bot] May 11, 2026
42933f4
Merge main into nightly-testing
mathlib-nightly-testing[bot] May 11, 2026
57b501d
chore: bump to nightly-2026-05-11 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] May 11, 2026
08b67ae
Merge remote-tracking branch 'origin/main' into bump/v4.31.0
May 11, 2026
04e72bf
chore: adaptations for nightly-2026-05-11
May 11, 2026
4ecac29
chore: adaptations for nightly-2026-05-11 (#560)
mathlib-nightly-testing[bot] May 11, 2026
7f084a1
Merge main into nightly-testing
mathlib-nightly-testing[bot] May 12, 2026
a8b1940
Merge main into nightly-testing
mathlib-nightly-testing[bot] May 12, 2026
a4c8522
chore: bump to nightly-2026-05-12 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] May 12, 2026
1d09642
Merge remote-tracking branch 'origin/main' into bump/v4.31.0
May 12, 2026
73d85eb
chore: adaptations for nightly-2026-05-12
May 12, 2026
5c33316
chore: adaptations for nightly-2026-05-12 (#565)
mathlib-nightly-testing[bot] May 12, 2026
0296078
Merge main into nightly-testing
mathlib-nightly-testing[bot] May 12, 2026
70d8177
chore: bump to nightly-2026-05-13 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] May 13, 2026
cb69c00
Merge remote-tracking branch 'origin/main' into bump/v4.31.0
May 13, 2026
0a07f6c
chore: adaptations for nightly-2026-05-13
May 13, 2026
aca6670
chore: adaptations for nightly-2026-05-13 (#566)
mathlib-nightly-testing[bot] May 13, 2026
d4e9f72
chore: bump to nightly-2026-05-14 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] May 14, 2026
7f36605
chore: adaptations for nightly-2026-05-14
May 14, 2026
36bca15
chore: adaptations for nightly-2026-05-14 (#567)
mathlib-nightly-testing[bot] May 14, 2026
6f72642
chore: bump to nightly-2026-05-17 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] May 17, 2026
b4f06d9
adaptations for lean4\#13651
chenson2018 May 17, 2026
b31f311
chore: adaptations for nightly-2026-05-17
May 17, 2026
f9dd275
chore: adaptations for nightly-2026-05-17 (#569)
mathlib-nightly-testing[bot] May 17, 2026
4c07832
Merge main into nightly-testing
mathlib-nightly-testing[bot] May 20, 2026
13ada78
Merge remote-tracking branch 'origin/main' into bump/v4.31.0
May 20, 2026
0f9c6a3
Merge commit 'b4f06d922a494e84caecf34b91436a68a44aafea' into bump/nig…
May 20, 2026
49499f8
chore: adaptations for nightly-2026-05-17
May 20, 2026
039b9f0
Merge branch 'bump/nightly-2026-05-17' into nightly-testing
May 20, 2026
6f17502
Merge main into nightly-testing
mathlib-nightly-testing[bot] May 20, 2026
78edf68
Merge main into nightly-testing
mathlib-nightly-testing[bot] May 20, 2026
4d9624d
Merge main into nightly-testing
mathlib-nightly-testing[bot] May 21, 2026
ab50ad7
Merge main into nightly-testing
mathlib-nightly-testing[bot] May 23, 2026
9ce3954
Merge main into nightly-testing
mathlib-nightly-testing[bot] May 23, 2026
5fabfb6
Merge main into nightly-testing
mathlib-nightly-testing[bot] May 24, 2026
1cb7da6
chore: bump to nightly-2026-05-25 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] May 25, 2026
c98dba9
conflict
chenson2018 May 25, 2026
8579adb
chore: adaptations for nightly-2026-05-25
chenson2018 May 25, 2026
811bbd1
chore: adaptations for nightly-2026-05-25 (#597)
chenson2018 May 25, 2026
de425ec
Merge main into nightly-testing
mathlib-nightly-testing[bot] May 26, 2026
dc75be2
Merge main into nightly-testing
mathlib-nightly-testing[bot] May 26, 2026
6e44702
Merge main into nightly-testing
mathlib-nightly-testing[bot] May 26, 2026
1471ef4
Merge main into nightly-testing
mathlib-nightly-testing[bot] May 28, 2026
65824cd
Merge main into nightly-testing
mathlib-nightly-testing[bot] May 28, 2026
2a6e2b2
chore: bump to nightly-2026-05-28 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] May 28, 2026
4d7ca70
rm extra instance variables
chenson2018 May 29, 2026
ada90ed
reducibility adjustments
chenson2018 May 29, 2026
49b2461
test adjustments
chenson2018 May 29, 2026
62ba811
conflict
chenson2018 May 29, 2026
8727fa5
conflict
chenson2018 May 29, 2026
cc08903
chore: adaptations for nightly-2026-05-28
chenson2018 May 29, 2026
4308349
Merge main into nightly-testing
mathlib-nightly-testing[bot] May 29, 2026
5425d3a
chore: bump toolchain to nightly-2026-05-29
Garmelon May 29, 2026
bd14a53
Merge main into nightly-testing
mathlib-nightly-testing[bot] May 29, 2026
09ffa2f
Merge main into nightly-testing
mathlib-nightly-testing[bot] Jun 1, 2026
3e827f1
chore: bump to nightly-2026-06-03 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Jun 3, 2026
17f9a0b
Merge remote-tracking branch 'origin/main' into bump/v4.32.0
Jun 3, 2026
4e3695a
chore: adaptations for nightly-2026-06-03
Jun 3, 2026
2921c1e
chore: adaptations for nightly-2026-06-03 (#614)
mathlib-nightly-testing[bot] Jun 3, 2026
61d8b9d
chore: bump to nightly-2026-06-04 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Jun 4, 2026
b8e8479
chore: adaptations for nightly-2026-06-04
Jun 4, 2026
cbe81f0
chore: adaptations for nightly-2026-06-04 (#616)
mathlib-nightly-testing[bot] Jun 4, 2026
a4c2cf1
chore: bump to nightly-2026-06-05 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Jun 5, 2026
1418547
chore: adaptations for nightly-2026-06-05
Jun 5, 2026
881fdb7
chore: adaptations for nightly-2026-06-05 (#618)
mathlib-nightly-testing[bot] Jun 5, 2026
8eca40c
chore: bump to nightly-2026-06-06 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Jun 6, 2026
1c8b5a9
chore: bump to nightly-2026-06-07 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Jun 7, 2026
d9a69f7
Merge main into nightly-testing
mathlib-nightly-testing[bot] Jun 7, 2026
e8dad13
Merge main into nightly-testing
mathlib-nightly-testing[bot] Jun 7, 2026
022ac0a
conflict
chenson2018 Jun 7, 2026
1f10fe3
chore: adaptations for nightly-2026-06-07
chenson2018 Jun 7, 2026
eff9eaa
chore: adaptations for nightly-2026-06-07 (#622)
chenson2018 Jun 7, 2026
1303251
Merge main into nightly-testing
mathlib-nightly-testing[bot] Jun 8, 2026
45e008c
Merge main into nightly-testing
mathlib-nightly-testing[bot] Jun 10, 2026
0b49978
Merge main into nightly-testing
mathlib-nightly-testing[bot] Jun 11, 2026
7a5ad21
Merge main into nightly-testing
mathlib-nightly-testing[bot] Jun 11, 2026
6857269
Merge main into nightly-testing
mathlib-nightly-testing[bot] Jun 12, 2026
a6946d0
chore: bump to nightly-2026-06-10 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Jun 12, 2026
414a171
Merge main into nightly-testing
mathlib-nightly-testing[bot] Jun 12, 2026
41d896a
Merge main into nightly-testing
mathlib-nightly-testing[bot] Jun 13, 2026
f907601
nolint -> set_option
chenson2018 Jun 13, 2026
0bb0dce
currently need both nolint and set_option
chenson2018 Jun 13, 2026
4c58025
conflict
chenson2018 Jun 13, 2026
e9ac112
chore: adaptations for nightly-2026-06-10
chenson2018 Jun 13, 2026
188bcde
chore: adaptations for nightly-2026-06-10 (#643)
chenson2018 Jun 13, 2026
b93d1ff
Merge main into nightly-testing
mathlib-nightly-testing[bot] Jun 13, 2026
9841f7b
Merge main into nightly-testing
mathlib-nightly-testing[bot] Jun 13, 2026
c613819
Merge main into nightly-testing
mathlib-nightly-testing[bot] Jun 15, 2026
6cfcefc
Merge main into nightly-testing
mathlib-nightly-testing[bot] Jun 16, 2026
b0edd6f
chore: bump to nightly-2026-06-15 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Jun 16, 2026
8676ecd
Merge remote-tracking branch 'origin/main' into bump/v4.32.0
chenson2018 Jun 16, 2026
d9685b4
chore: adaptations for nightly-2026-06-15
chenson2018 Jun 16, 2026
02adaf5
chore: adaptations for nightly-2026-06-15 (#656)
chenson2018 Jun 16, 2026
1e03667
chore: bump to nightly-2026-06-16 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Jun 16, 2026
71b12f3
chore: adaptations for nightly-2026-06-16
Jun 16, 2026
a579bc5
Merge main into nightly-testing
mathlib-nightly-testing[bot] Jun 19, 2026
e831cd6
chore: bump to nightly-2026-06-19 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Jun 19, 2026
7318506
Merge main into nightly-testing
mathlib-nightly-testing[bot] Jun 19, 2026
dde0b69
chore: adaptations for nightly-2026-06-19
Jun 19, 2026
c709caf
Merge branch 'bump/nightly-2026-06-19' into nightly-testing
Jun 19, 2026
1978d13
Merge main into nightly-testing
mathlib-nightly-testing[bot] Jun 20, 2026
6ce98ca
Merge main into nightly-testing
mathlib-nightly-testing[bot] Jun 21, 2026
198edc0
Merge main into nightly-testing
mathlib-nightly-testing[bot] Jun 22, 2026
b21cb56
chore: bump to nightly-2026-06-21 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Jun 22, 2026
05389b4
chore: bump to nightly-2026-06-22 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Jun 22, 2026
022b39a
chore: adaptations for nightly-2026-06-22
chenson2018 Jun 22, 2026
2f505c5
Merge main into nightly-testing
mathlib-nightly-testing[bot] Jun 22, 2026
668df1c
chore: bump to nightly-2026-06-23 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Jun 23, 2026
bddbd7c
chore: adaptations for nightly-2026-06-23
Jun 23, 2026
c3cb40c
chore: bump to nightly-2026-06-24 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Jun 24, 2026
c6e686e
chore: adaptations for nightly-2026-06-24
Jun 24, 2026
85234d2
chore: bump to nightly-2026-06-25 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Jun 25, 2026
a1b8541
chore: adaptations for nightly-2026-06-25
Jun 25, 2026
ecdfb61
Merge main into nightly-testing
mathlib-nightly-testing[bot] Jun 25, 2026
171aa38
Merge main into nightly-testing
mathlib-nightly-testing[bot] Jun 26, 2026
e43be33
chore: bump to nightly-2026-06-27 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Jun 28, 2026
0b678bb
chore: adaptations for nightly-2026-06-27
Jun 28, 2026
30fd2b5
Merge main into nightly-testing
mathlib-nightly-testing[bot] Jul 1, 2026
340658d
chore: bump to nightly-2026-06-30 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Jul 1, 2026
1af3493
chore: adaptations for nightly-2026-06-30
Jul 1, 2026
196d4bc
chore: bump to nightly-2026-07-01 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Jul 1, 2026
edca0b7
Merge main into nightly-testing
mathlib-nightly-testing[bot] Jul 2, 2026
5063327
chore: bump to nightly-2026-07-02 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Jul 2, 2026
2339674
chore: bump to nightly-2026-07-03 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Jul 4, 2026
d065086
chore: adaptations for nightly-2026-07-03
chenson2018 Jul 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": "f29707919d03b8ad12f6f486e2bbf98f908fd331",
"rev": "ce52fd18b8ecea2a6268f6973e3ca54f687a01c1",
"name": "mathlib",
"manifestFile": "lake-manifest.json",
"inputRev": "nightly-testing-2026-06-30",
"inputRev": "nightly-testing-2026-07-03",
"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": "27d322d17a18e76985a24ab17092c3d241711ea3",
"rev": "8fb9f43f0c722dffce4a00b38adf12a5043a4936",
"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-06-30"
rev = "nightly-testing-2026-07-03"

[[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-06-30
leanprover/lean4:nightly-2026-07-03
Loading