chore: update to lean v4.26.0-rc2 and latest verso

book/.verso/verso-xref-manifest.json

@@ -1,8 +1,7 @@
 {"version": 0,
  "sources":
  {"manual":
-  {"updated": "2025-10-23:16:40:12.244921000",
-   "updateFrequency": "manual",
+  {"updateFrequency": "manual",
    "shortName": "ref",
    "root": "https://lean-lang.org/doc/reference/4.23.0/",
    "longName": "Lean Language Reference"}},

book/FPLean/Examples.lean

@@ -383,17 +383,17 @@ private def quoteCode (str : String) : String := Id.run do
   let str := if str.startsWith "`" || str.endsWith "`" then " " ++ str ++ " " else str
   let mut n := 1
   let mut run := none
-  let mut iter := str.iter
-  while h : iter.hasNext do
-    let c := iter.curr' h
-    iter := iter.next
+  let mut iter := str.startValidPos
+  while h : iter ≠ str.endValidPos do
+    let c := iter.get h
+    iter := iter.next h
     if c == '`' then
       run := some (run.getD 0 + 1)
     else if let some k := run then
       if k > n then n := k
       run := none
 
-  let delim := String.mk (List.replicate n '`')
+  let delim := String.ofList (List.replicate n '`')
   return delim ++ str ++ delim
 
 
@@ -469,10 +469,10 @@ where
   delims : String := Id.run do
     let mut n := 3
     let mut run := none
-    let mut iter := newContents.iter
-    while h : iter.hasNext do
-      let c := iter.curr' h
-      iter := iter.next
+    let mut iter := newContents.startValidPos
+    while h : iter ≠ newContents.endValidPos do
+      let c := iter.get h
+      iter := iter.next h
       if c == '`' then
         run := some (run.getD 0 + 1)
       else if let some k := run then
@@ -927,17 +927,17 @@ where
     let str := if str.startsWith "`" || str.endsWith "`" then " " ++ str ++ " " else str
     let mut n := 1
     let mut run := none
-    let mut iter := str.iter
-    while h : iter.hasNext do
-      let c := iter.curr' h
-      iter := iter.next
+    let mut iter := str.startValidPos
+    while h : iter ≠ str.endValidPos do
+      let c := iter.get h
+      iter := iter.next h
       if c == '`' then
         run := some (run.getD 0 + 1)
       else if let some k := run then
         if k > n then n := k
         run := none
 
-    let delim := String.mk (List.replicate n '`')
+    let delim := String.ofList (List.replicate n '`')
     return delim ++ str ++ delim
 
 macro_rules
@@ -956,19 +956,19 @@ macro_rules
 
 
 def hasSubstring (s pattern : String) : Bool :=
-  if h : pattern.endPos.1 = 0 then false
+  if h : pattern.rawEndPos.1 = 0 then false
   else
     have hPatt := Nat.zero_lt_of_ne_zero h
     let rec loop (pos : String.Pos.Raw) :=
-      if h : pos.byteIdx + pattern.endPos.byteIdx > s.endPos.byteIdx then
+      if h : pos.byteIdx + pattern.rawEndPos.byteIdx > s.rawEndPos.byteIdx then
         false
       else
         have := Nat.lt_of_lt_of_le (Nat.add_lt_add_left hPatt _) (Nat.ge_of_not_lt h)
-        if pos.substrEq s pattern 0 pattern.endPos.byteIdx then
+        if pos.substrEq s pattern 0 pattern.rawEndPos.byteIdx then
           have := Nat.sub_lt_sub_left this (Nat.add_lt_add_left hPatt _)
           true
         else
           have := Nat.sub_lt_sub_left this (pos.byteIdx_lt_byteIdx_next s)
           loop (pos.next s)
-      termination_by s.endPos.1 - pos.1
+      termination_by s.rawEndPos.1 - pos.1
     loop 0

book/FPLean/Examples/Commands/ShLex.lean

@@ -8,12 +8,12 @@ private inductive State where
 
 def shlex (cmd : String) : Except String (Array String) := do
   let mut state : State := .normal
-  let mut iter := cmd.iter
+  let mut iter := cmd.startValidPos
   let mut out : Array String := #[]
   let mut current : Option String := none
-  while h : iter.hasNext do
-    let c := iter.curr' h
-    iter := iter.next' h
+  while h : iter ≠ cmd.endValidPos do
+    let c := iter.get h
+    iter := iter.next h
     match state, c with
     | .normal, '\\' =>
       state := .escaped state

book/Main.lean

@@ -16,7 +16,7 @@ def config : Config where
   emitHtmlMulti := true
   htmlDepth := 2
   extraFiles := [("static", "static")]
-  extraCss := [
+  extraCss := Std.HashSet.ofList [
     "/static/theme.css",
     "/static/fonts/source-serif/source-serif-text.css",
     "/static/fonts/source-code-pro/source-code-pro.css",

book/lake-manifest.json

@@ -5,17 +5,27 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "b1cdd66be1f055926796aa804fdc13c9e9ac17c6",
+   "rev": "c5f95b7296ee0d6ecfadd346c457e75cb838e853",
    "name": "verso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": false,
    "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/plausible",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "ec4a54b5308c1f46b4b52a9c62fb67d193aa0972",
+   "name": "plausible",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/acmepjz/md4lean",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "66aefec2852d3e229517694e642659f316576591",
+   "rev": "38ac5945d744903ffcc473ce1030223991b11cf6",
    "name": "MD4Lean",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "57f4e6c99a4132d54a2105dec21c2e3c2af98b15",
+   "rev": "519b262cfc93634f904c9fb0992a45377ee49a9d",
    "name": "subverso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

book/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.25.0-rc2
+leanprover/lean4:v4.26.0-rc2