chore: bump toolchain to 2026-07-08 (#885)

Remove Char.utf16Size because it got moved into the `Lean` namespace in
leanprover/lean4#14307, and modify the example
for "Missing `WPMonad` Instance" to avoid problems with
implicit_reducible changes.

Author: robsimmons

Manual/BasicTypes/Char.lean

@@ -180,5 +180,3 @@ tag := "char-api-classes"
 ## Unicode
 
 {docstring Char.utf8Size}
-
-{docstring Char.utf16Size}

Manual/VCGen.lean

@@ -444,25 +444,24 @@ set_option mvcgen.warning false
 
 ```
 
-This reimplementation of {name}`Id` has a {name}`WP` instance, but no {name}`WPMonad` instance:
+The single-field structure {name}`Identity` acts like the identity monad {name}`Id`. It has a {name}`WP` instance, but no {name}`WPMonad` instance:
 ```lean
-def Identity (α : Type u) : Type u := α
+structure Identity (α : Type u) where
+  run : α
 
 variable {α : Type u}
 
-def Identity.run (act : Identity α) : α := act
-
 instance : Monad Identity where
-  pure x := x
-  bind x f := f x
+  pure x := ⟨x⟩
+  bind x f := f x.run
 
 instance : WP Identity .pure where
-  wp x := PredTrans.pure x
+  wp x := PredTrans.pure x.run
 
 theorem Identity.of_wp_run_eq {x : α} {prog : Identity α}
     (h : Identity.run prog = x) (P : α → Prop) :
     (⊢ₛ wp⟦prog⟧ (⇓ a => ⟨P a⟩)) → P x := by
-  simp_all [WP.wp, Identity.run, ← h]
+  simp_all [WP.wp, ← h]
 ```
 
 ```lean -show

lake-manifest.json

@@ -19,7 +19,7 @@
    "name": "illuminate",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
-   "inherited": true,
+   "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/verso-web-components",
    "type": "git",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2026-07-03
+leanprover/lean4:nightly-2026-07-08