chore: adapt to leanprover/lean4#11587

Author: Kha

Aesop/BuiltinRules/DestructProducts.lean

@@ -84,7 +84,7 @@ private meta def destructProductHyp? (goal : MVarId) (hyp : FVarId)
         (preserveBinderNames := true) (useNamesForExplicitOnly := false)
       return (goal, lName, rName)
 
-meta def destructProductsCore (goal : MVarId) (md : TransparencyMode) :
+meta partial def destructProductsCore (goal : MVarId) (md : TransparencyMode) :
     BaseM (MVarId × Array LazyStep) := do
   let result ← go 0 goal |>.run
   if result.fst == goal then

Aesop/BuiltinRules/Split.lean

@@ -24,7 +24,7 @@ meta def splitTarget : RuleTac := RuleTac.ofSingleRuleTac λ input => do
   let goals ← goals.mapM (mvarIdToSubgoal input.goal ·)
   return (goals, steps, none)
 
-meta def splitHypothesesCore (goal : MVarId) :
+meta partial def splitHypothesesCore (goal : MVarId) :
     ScriptM (Option (Array MVarId)) :=
   withIncRecDepth do
   let some goals ← splitFirstHypothesisS? goal

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2025-12-03
+leanprover/lean4-pr-releases:pr-release-11587-3a37d68