Skip to content

Commit e0573fb

Browse files
Garmelonmathlib4-botmathlib-nightly-testing[bot]leanprover-community-mathlib4-botkim-em
authored
chore: bump toolchain to v4.32.0-rc1 (#664)
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: mathlib-nightly-testing[bot] <258991302+mathlib-nightly-testing[bot]@users.noreply.github.com> Co-authored-by: mathlib-nightly-testing[bot] <mathlib-nightly-testing[bot]@users.noreply.github.com> Co-authored-by: leanprover-community-mathlib4-bot <129911861+leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Chris Henson <chrishenson.net@gmail.com> Co-authored-by: Ching-Tsun Chou <chingtsun.chou@gmail.com> Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com> Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com> Co-authored-by: Alexandre Rademaker <arademaker@gmail.com> Co-authored-by: Fabrizio Montesi <famontesi@gmail.com>
1 parent 1dbda53 commit e0573fb

4 files changed

Lines changed: 13 additions & 12 deletions

File tree

Cslib/Foundations/Semantics/LTS/LTSCat/Basic.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -35,6 +35,7 @@ def LTS.withIdle (lts : LTS State Label) : LTS State (Option Label) :=
3535

3636
/-! ## LTSs and LTS morphisms form a category -/
3737

38+
set_option linter.checkUnivs false in
3839
/--
3940
The definition of labelled transition system (with the type of states and the
4041
type of labels as part of the structure).

lake-manifest.json

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -5,17 +5,17 @@
55
"type": "git",
66
"subDir": null,
77
"scope": "leanprover-community",
8-
"rev": "fabf563a7c95a166b8d7b6efca11c8b4dc9d911f",
8+
"rev": "360da6fa66c1273b76b6b2d8c5666fd5ac2e3b56",
99
"name": "mathlib",
1010
"manifestFile": "lake-manifest.json",
11-
"inputRev": "fabf563a7c95a166b8d7b6efca11c8b4dc9d911f",
11+
"inputRev": "360da6fa66c1273b76b6b2d8c5666fd5ac2e3b56",
1212
"inherited": false,
1313
"configFile": "lakefile.lean"},
1414
{"url": "https://github.com/leanprover-community/plausible",
1515
"type": "git",
1616
"subDir": null,
1717
"scope": "leanprover-community",
18-
"rev": "63045536fe95024e6c18fc7b48e03f506701c5bc",
18+
"rev": "f3f26cc72646205ca167117487c008ee1dafe816",
1919
"name": "plausible",
2020
"manifestFile": "lake-manifest.json",
2121
"inputRev": "main",
@@ -35,7 +35,7 @@
3535
"type": "git",
3636
"subDir": null,
3737
"scope": "leanprover-community",
38-
"rev": "5c7542ed018c78194f1e2b903eaf6a792b74c03d",
38+
"rev": "41f407a8e85b0fdc00910633a8f14754139b63f4",
3939
"name": "importGraph",
4040
"manifestFile": "lake-manifest.json",
4141
"inputRev": "main",
@@ -45,7 +45,7 @@
4545
"type": "git",
4646
"subDir": null,
4747
"scope": "leanprover-community",
48-
"rev": "24b0d9dc081c5423f8eec7e866c441e5184f29d9",
48+
"rev": "e6518a674e62de322b8f79eebeda7bcae2a36bc3",
4949
"name": "proofwidgets",
5050
"manifestFile": "lake-manifest.json",
5151
"inputRev": "main",
@@ -55,7 +55,7 @@
5555
"type": "git",
5656
"subDir": null,
5757
"scope": "leanprover-community",
58-
"rev": "e3cb2f741431ce31bf73549fb52316a57368b06f",
58+
"rev": "b5b9e2bb45ce91e4bc44eaa738c3a8910404ab82",
5959
"name": "aesop",
6060
"manifestFile": "lake-manifest.json",
6161
"inputRev": "master",
@@ -65,7 +65,7 @@
6565
"type": "git",
6666
"subDir": null,
6767
"scope": "leanprover-community",
68-
"rev": "f46324995fca5f0483b742e4eb4daec7f4ee50d2",
68+
"rev": "7a62bd13860cd39ac98da16ffc8c24d601353f69",
6969
"name": "Qq",
7070
"manifestFile": "lake-manifest.json",
7171
"inputRev": "master",
@@ -75,7 +75,7 @@
7575
"type": "git",
7676
"subDir": null,
7777
"scope": "leanprover-community",
78-
"rev": "fa08db58b30eb033edcdab331bba000827f9f785",
78+
"rev": "954dbc9873f3b4534dc9896604593406d0383520",
7979
"name": "batteries",
8080
"manifestFile": "lake-manifest.json",
8181
"inputRev": "main",
@@ -85,10 +85,10 @@
8585
"type": "git",
8686
"subDir": null,
8787
"scope": "leanprover",
88-
"rev": "92564e5770e4d09f2d86dfbf8ada1e9c715b384c",
88+
"rev": "406ebb8c8e2f7e852a1b47764b42494022ce652c",
8989
"name": "Cli",
9090
"manifestFile": "lake-manifest.json",
91-
"inputRev": "v4.31.0",
91+
"inputRev": "v4.32.0-rc1",
9292
"inherited": true,
9393
"configFile": "lakefile.toml"}],
9494
"name": "cslib",

lakefile.toml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@ weak.linter.unicodeLinter = false
1818
[[require]]
1919
name = "mathlib"
2020
scope = "leanprover-community"
21-
rev = "fabf563a7c95a166b8d7b6efca11c8b4dc9d911f"
21+
rev = "360da6fa66c1273b76b6b2d8c5666fd5ac2e3b56"
2222

2323
[[lean_lib]]
2424
name = "Cslib"

lean-toolchain

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
leanprover/lean4:v4.31.0
1+
leanprover/lean4:v4.32.0-rc1

0 commit comments

Comments
 (0)