chore: bump to v4.14.0-rc1

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2024-10-30
+leanprover/lean4:v4.14.0-rc1

src/examples/SubVerso/Examples/Slice.lean

@@ -235,9 +235,9 @@ def sliceSyntax [Monad m] [MonadEnv m] [MonadError m] [MonadFileMap m] (stx : Sy
   let env ← getEnv
   let mut sliced : HashMap String Syntax := {}
   for (s, _) in ss.toArray do
-    let rem := ss.erase s |>.toList |>.bind (·.snd.toList) |>.toArray
+    let rem := ss.erase s |>.toList |>.flatMap (·.snd.toList) |>.toArray
     sliced := sliced.insert s (removeRanges env rem stx')
-  let residual := removeRanges env (ss.toList.bind (·.snd.toList) |>.toArray) stx'
+  let residual := removeRanges env (ss.toList.flatMap (·.snd.toList) |>.toArray) stx'
 
   return {original := stx, residual, sliced}
 

src/highlighting/SubVerso/Highlighting/Code.lean

@@ -701,7 +701,7 @@ partial def findTactics
 
   -- Override states - some tactics show many intermediate states, which is overwhelming in rendered
   -- output. Get the right one to show for the whole thing, then adjust its positioning.
-  if let `(tactic|rw $[$_c:config]? [$_rs,*]%$brak $[$_l:location]?) := stx then
+  if let `(tactic|rw $_c:optConfig [$_rs,*]%$brak $[$_l:location]?) := stx then
     if let some (goals, _startPos, _endPos, _endPosition) ← findTactics ids trees brak then
       return some (goals, startPos.byteIdx, endPos.byteIdx, endPosition)