From 7c298b14ede5964ad5d5ba7d215ef2a77b5af559 Mon Sep 17 00:00:00 2001 From: Joscha Date: Mon, 10 Aug 2026 19:51:50 +0200 Subject: [PATCH 1/2] chore: adaptations from downstream-lean4 --- Test.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Test.lean b/Test.lean index bd74231..c692774 100644 --- a/Test.lean +++ b/Test.lean @@ -725,8 +725,8 @@ _private.Init.Prelude.0.isValidChar_UInt32.match_1_1 Nat.lt_trans Decidable.decide _private.Init.Prelude.0.of_decide_eq_true.match_1_1 -_private.Init.Prelude.0.ne_true_of_eq_false.match_1_1 -ne_true_of_eq_false +_private.Init.Prelude.0.Bool.ne_true_of_eq_false.match_1_1 +Bool.ne_true_of_eq_false _private.Init.Prelude.0.decide_eq_false.match_1_1 decide_eq_false of_decide_eq_true From bbfb869094ae2c14cc445f86ad2977dab7c12f14 Mon Sep 17 00:00:00 2001 From: Joscha Date: Mon, 10 Aug 2026 19:51:50 +0200 Subject: [PATCH 2/2] chore: bump toolchain to v4.34.0-rc1 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 025e595..75def60 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.33.0 +leanprover/lean4:v4.34.0-rc1