From a35f1b48150e5fc43d4c66fad7bc2790bce91409 Mon Sep 17 00:00:00 2001 From: Joscha Date: Tue, 15 Sep 2026 17:39:47 +0200 Subject: [PATCH 1/2] chore: adaptations from downstream-lean4 --- Test.lean | 46 +++++++++++++++++++++++++--------------------- 1 file changed, 25 insertions(+), 21 deletions(-) diff --git a/Test.lean b/Test.lean index c692774..c3a46da 100644 --- a/Test.lean +++ b/Test.lean @@ -494,37 +494,32 @@ List.map._f List.map List.flatMap Char.val +Bool +Bool.false +Bool.true +Bool.rec +Bool.casesOn +Bool.Reflects.match_1 False False.rec Not +Bool.Reflects Decidable -Decidable.isFalse -Decidable.isTrue +Decidable.intro Decidable.rec -Decidable.casesOn +Decidable.decide +Decidable.reflects_decide +dite ite LE LE.mk LE.rec LE.le instLENat -dite -Bool -Bool.false -Bool.true -Bool.rec Nat.ble.match_1 Nat.ble._f Nat.ble -DecidableEq -Bool.casesOn -Bool.decEq.match_1 -rfl -Bool.noConfusionType -Eq.ndrec -Bool.noConfusion -Bool.decEq -instDecidableEqBool +Nat.decEq.match_1 False.elim Eq.casesOn HEq @@ -539,6 +534,7 @@ Nat.beq _private.Init.Prelude.0.noConfusion_of_Nat.aux.match_1_1 _private.Init.Prelude.0.noConfusion_of_Nat.aux._f _private.Init.Prelude.0.noConfusion_of_Nat.aux +rfl congrArg noConfusion_of_Nat Bool.ctorIdx @@ -552,6 +548,7 @@ Nat.le.below.step Nat.le.below.rec Nat.le.brecOn Nat.le.below.casesOn +Eq.ndrec Eq.symm cast eq_of_heq @@ -579,6 +576,9 @@ Nat.ble_succ_eq_true._f Nat.ble_succ_eq_true Nat.ble_eq_true_of_le Nat.not_le_of_not_ble_eq_true +Bool.noConfusionType +Bool.noConfusion +Nat.decLe._proof_1 Nat.decLe HMod HMod.mk @@ -644,10 +644,12 @@ Nat.mod Nat.instMod _private.Init.Prelude.0.Nat.mod_lt.match_1_3 Nat.zero_lt_succ +Decidable.casesOn _private.Init.Prelude.0.Nat.mod_lt.match_1_1 _private.Init.Prelude.0.Nat.modCore_lt.match_1_1 Nat.not_lt_zero _private.Init.Prelude.0.Nat.modCoreGo_lt.match_1_1 +Decidable.isTrue Or.casesOn _private.Init.Prelude.0.Or.elim.match_1_1 Or.elim @@ -665,6 +667,7 @@ Nat.eq_or_lt_of_le Nat.lt_or_ge._f Nat.lt_or_ge Nat.lt_of_not_le +Decidable.isFalse Nat.modCoreGo_lt Nat.modCore_lt Nat.mod_lt @@ -710,20 +713,21 @@ ByteArray.IsValidUTF8.rec String String.ofByteArray String.rec -instDecidableAnd.match_1 +Bool.or +instDecidableOr.match_3 instDecidableOr.match_1 instDecidableOr._proof_1 instDecidableOr +Bool.and +instDecidableAnd.match_1 And.right -instDecidableAnd._proof_1 And.left -instDecidableAnd._proof_2 +instDecidableAnd._proof_1 instDecidableAnd BitVec.ofNatLT UInt32.size _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.Bool.ne_true_of_eq_false.match_1_1 Bool.ne_true_of_eq_false From eb23020eafbd1e0241a9683f85b11a8135623db6 Mon Sep 17 00:00:00 2001 From: Joscha Date: Tue, 15 Sep 2026 17:39:47 +0200 Subject: [PATCH 2/2] chore: bump toolchain to v4.35.0-rc1 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 12359f9..3d1dc1d 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.34.0 +leanprover/lean4:v4.35.0-rc1