feat: implement grind_annotated command

- Add syntax declaration in Init/Grind/Annotated.lean
- Add elaborator with YYYY-MM-DD date validation in Lean/Elab/Tactic/Grind/Annotated.lean
- Add SimplePersistentEnvExtension to track grind-annotated modules
- Add filterGrindAnnotated wrapper for Selector
- Apply filter to sineQuaNonSelector in default library suggestions
- Set caller field to "grind" when grind tactic calls LibrarySuggestions

.claude/CLAUDE.md

@@ -1,34 +1,14 @@
-To build Lean you should use `make -j -C build/release`.
-
-To run a test you should use `cd tests/lean/run && ./test_single.sh example_test.lean`.
-
-## New features
-
 When asked to implement new features:
 * begin by reviewing existing relevant code and tests
 * write comprehensive tests first (expecting that these will initially fail)
 * and then iterate on the implementation until the tests pass.
 
-All new tests should go in `tests/lean/run/`. These tests don't have expected output; we just check there are no errors. You should use `#guard_msgs` to check for specific messages.
+To build Lean you should use `make -j$(nproc) -C build/release`.
 
-## Success Criteria
+To run a test you should use `cd tests/lean/run && ./test_single.sh example_test.lean`.
 
-*Never* report success on a task unless you have verified both a clean build without errors, and that the relevant tests pass.
+*Never* report success on a task unless you have verified both a clean build without errors, and that the relevant tests pass. You have to keep working until you have verified both of these.
 
-## Build System Safety
+All new tests should go in `tests/lean/run/`. Note that these tests don't have expected output, and just run on a success or failure basis. So you should use `#guard_msgs` to check for specific messages.
 
-**NEVER manually delete build directories** (build/, stage0/, stage1/, etc.) even when builds fail.
-- ONLY use the project's documented build command: `make -j -C build/release`
-- If a build is broken, ask the user before attempting any manual cleanup
-
-## LSP and IDE Diagnostics
-
-After rebuilding, LSP diagnostics may be stale until the user interacts with files. Trust command-line test results over IDE diagnostics.
-
-## Update prompting when the user is frustrated
-
-If the user expresses frustration with you, stop and ask them to help update this `.claude/CLAUDE.md` file with missing guidance.
-
-## Creating pull requests.
-
-All PRs must have a first paragraph starting with "This PR". This paragraph is automatically incorporated into release notes. Read `lean4/doc/dev/commit_convention.md` when making PRs.
+If you are not following best practices specific to this repository and the user expresses frustration, stop and ask them to help update this `.claude/CLAUDE.md` file with the missing guidance.

.github/workflows/ci.yml

@@ -106,54 +106,9 @@ jobs:
           TAG_NAME="${GITHUB_REF##*/}"
           echo "RELEASE_TAG=$TAG_NAME" >> "$GITHUB_OUTPUT"
 
-      - name: Validate CMakeLists.txt version matches tag
-        if: steps.set-release.outputs.RELEASE_TAG != ''
-        run: |
-          echo "Validating CMakeLists.txt version matches tag ${{ steps.set-release.outputs.RELEASE_TAG }}"
-
-          # Extract version values from CMakeLists.txt
-          CMAKE_MAJOR=$(grep -E "^set\(LEAN_VERSION_MAJOR " src/CMakeLists.txt | grep -oE '[0-9]+')
-          CMAKE_MINOR=$(grep -E "^set\(LEAN_VERSION_MINOR " src/CMakeLists.txt | grep -oE '[0-9]+')
-          CMAKE_PATCH=$(grep -E "^set\(LEAN_VERSION_PATCH " src/CMakeLists.txt | grep -oE '[0-9]+')
-          CMAKE_IS_RELEASE=$(grep -E "^set\(LEAN_VERSION_IS_RELEASE " src/CMakeLists.txt | grep -oE '[0-9]+')
-
-          # Expected values from tag parsing
-          TAG_MAJOR="${{ steps.set-release.outputs.LEAN_VERSION_MAJOR }}"
-          TAG_MINOR="${{ steps.set-release.outputs.LEAN_VERSION_MINOR }}"
-          TAG_PATCH="${{ steps.set-release.outputs.LEAN_VERSION_PATCH }}"
-
-          ERRORS=""
-
-          if [[ "$CMAKE_MAJOR" != "$TAG_MAJOR" ]]; then
-            ERRORS+="LEAN_VERSION_MAJOR: expected $TAG_MAJOR, found $CMAKE_MAJOR\n"
-          fi
-          if [[ "$CMAKE_MINOR" != "$TAG_MINOR" ]]; then
-            ERRORS+="LEAN_VERSION_MINOR: expected $TAG_MINOR, found $CMAKE_MINOR\n"
-          fi
-          if [[ "$CMAKE_PATCH" != "$TAG_PATCH" ]]; then
-            ERRORS+="LEAN_VERSION_PATCH: expected $TAG_PATCH, found $CMAKE_PATCH\n"
-          fi
-          if [[ "$CMAKE_IS_RELEASE" != "1" ]]; then
-            ERRORS+="LEAN_VERSION_IS_RELEASE: expected 1, found $CMAKE_IS_RELEASE\n"
-          fi
-
-          if [[ -n "$ERRORS" ]]; then
-            echo "::error::Version mismatch between tag and src/CMakeLists.txt"
-            echo ""
-            echo "Tag ${{ steps.set-release.outputs.RELEASE_TAG }} expects version $TAG_MAJOR.$TAG_MINOR.$TAG_PATCH"
-            echo "But src/CMakeLists.txt has mismatched values:"
-            echo -e "$ERRORS"
-            echo ""
-            echo "Fix src/CMakeLists.txt, delete the tag, and re-tag."
-            exit 1
-          fi
-
-          echo "Version validation passed: $TAG_MAJOR.$TAG_MINOR.$TAG_PATCH"
-
       # 0: PRs without special label
       # 1: PRs with `merge-ci` label, merge queue checks, master commits
-      # 2: nightlies
-      # 3: PRs with `release-ci` label, full releases
+      # 2: PRs with `release-ci` label, releases (incl. nightlies)
       - name: Set check level
         id: set-level
         # We do not use github.event.pull_request.labels.*.name here because
@@ -163,16 +118,14 @@ jobs:
           check_level=0
           fast=false
 
-          if [[ -n "${{ steps.set-release.outputs.RELEASE_TAG }}" || -n "${{ steps.set-release-custom.outputs.RELEASE_TAG }}" ]]; then
-            check_level=3
-          elif [[ -n "${{ steps.set-nightly.outputs.nightly }}" ]]; then
+          if [[ -n "${{ steps.set-nightly.outputs.nightly }}" || -n "${{ steps.set-release.outputs.RELEASE_TAG }}" || -n "${{ steps.set-release-custom.outputs.RELEASE_TAG }}" ]]; then
             check_level=2
           elif [[ "${{ github.event_name }}" != "pull_request" ]]; then
             check_level=1
           else
             labels="$(gh api repos/${{ github.repository_owner }}/${{ github.event.repository.name }}/pulls/${{ github.event.pull_request.number }} --jq '.labels')"
             if echo "$labels" | grep -q "release-ci"; then
-              check_level=3
+              check_level=2
             elif echo "$labels" | grep -q "merge-ci"; then
               check_level=1
             fi
@@ -257,22 +210,17 @@ jobs:
                 "test": true,
                 "CMAKE_PRESET": "reldebug",
               },
-              {
+              // TODO: suddenly started failing in CI
+              /*{
                 "name": "Linux fsanitize",
-                // Always run on large if available, more reliable regarding timeouts
-                "os": large ? "nscloud-ubuntu-22.04-amd64-8x16-with-cache" : "ubuntu-latest",
+                "os": "ubuntu-latest",
                 "enabled": level >= 2,
-                // do not fail nightlies on this for now
-                "secondary": level <= 2,
                 "test": true,
                 // turn off custom allocator & symbolic functions to make LSAN do its magic
                 "CMAKE_PRESET": "sanitize",
-                // `StackOverflow*` correctly triggers ubsan
-                // `reverse-ffi` fails to link in sanitizers
-                // `interactive` and `async_select_channel` fail nondeterministically, would need to
-                // be investigated.
-                "CTEST_OPTIONS": "-E 'StackOverflow|reverse-ffi|interactive|async_select_channel'"
-              },
+                // exclude seriously slow/problematic tests (laketests crash)
+                "CTEST_OPTIONS": "-E 'interactivetest|leanpkgtest|laketest|benchtest'"
+              },*/
               {
                 "name": "macOS",
                 "os": "macos-15-intel",
@@ -304,7 +252,7 @@ jobs:
               },
               {
                 "name": "Windows",
-                "os": large && (fast || level >= 2) ? "namespace-profile-windows-amd64-4x16" : "windows-2022",
+                "os": large && (fast || level == 2) ? "namespace-profile-windows-amd64-4x16" : "windows-2022",
                 "release": true,
                 "enabled": level >= 2,
                 "test": true,

CMakePresets.json

@@ -41,7 +41,7 @@
         "SMALL_ALLOCATOR": "OFF",
         "USE_MIMALLOC": "OFF",
         "BSYMBOLIC": "OFF",
-        "LEAN_TEST_VARS": "MAIN_STACK_SIZE=16000 LSAN_OPTIONS=max_leaks=10"
+        "LEAN_TEST_VARS": "MAIN_STACK_SIZE=16000"
       },
       "generator": "Unix Makefiles",
       "binaryDir": "${sourceDir}/build/sanitize"

doc/dev/bootstrap.md

@@ -72,9 +72,6 @@ update the archived C source code of the stage 0 compiler in `stage0/src`.
 
 The github repository will automatically update stage0 on `master` once
 `src/stdlib_flags.h` and `stage0/src/stdlib_flags.h` are out of sync.
-To trigger this, modify `stage0/src/stdlib_flags.h` (e.g., by adding or changing
-a comment). When `update-stage0` runs, it will overwrite `stage0/src/stdlib_flags.h`
-with the contents of `src/stdlib_flags.h`, bringing them back in sync.
 
 NOTE: A full rebuild of stage 1 will only be triggered when the *committed* contents of `stage0/` are changed.
 Thus if you change files in it manually instead of through `update-stage0-commit` (see below) or fetching updates from git, you either need to commit those changes first or run `make -C build/release clean-stdlib`.

releases_drafts/module-system.md

@@ -1,54 +0,0 @@
-This release introduces the Lean module system, which allows files to
-control the visibility of their contents for other files. In previous
-releases, this feature was available as a preview when the option
-`experimental.module` was set to `true`; it is now a fully supported
-feature of Lean.
-
-# Benefits
-
-Because modules reduce the amount of information exposed to other
-code, they speed up rebuilds because irrelevant changes can be
-ignored, they make it possible to be deliberate about API evolution by
-hiding details that may change from clients, they help proofs be
-checked faster by avoiding accidentally unfolding definitions, and
-they lead to smaller executable files through improved dead code
-elimination.
-
-# Visibility
-
-A source file is a module if it begins with the `module` keyword.  By
-default, declarations in a module are private; the `public` modifier
-exports them. Proofs of theorems and bodies of definitions are private
-by default even when their signatures are public; the bodies of
-definitions can be made public by adding the `@[expose]`
-attribute. Theorems and opaque constants never expose their bodies.
-
-`public section` and `@[expose] section` change the default visibility
-of declarations in the section.
-
-# Imports
-
-Modules may only import other modules. By default, `import` adds the
-public information of the imported module to the private scope of the
-current module. Adding the `public` modifier to an import places the
-imported modules's public information in the public scope of the
-current module, exposing it in turn to the current module's clients.
-
-Within a package, `import all` can be used to import another module's
-private scope into the current module; this can be used to separate
-lemmas or tests from definition modules without exposing details to
-downstream clients.
-
-# Meta Code
-
-Code used in metaprograms must be marked `meta`. This ensures that the
-code is compiled and available for execution when it is needed during
-elaboration. Meta code may only reference other meta code. A whole
-module can be made available in the meta phase using `meta import`;
-this allows code to be shared across phases by importing the module in
-each phase. Code that is reachable from public metaprograms must be
-imported via `public meta import`, while local metaprograms can use
-plain `meta import` for their dependencies.
-
-
-The module system is described in detail in [the Lean language reference](https://lean-reference-manual-review.netlify.app/find/?domain=Verso.Genre.Manual.section&name=files).

script/Shake.lean

@@ -300,7 +300,7 @@ def parseHeaderFromString (text path : String) :
     throw <| .userError "parse errors in file"
   -- the insertion point for `add` is the first newline after the imports
   let insertion := header.raw.getTailPos?.getD parserState.pos
-  let insertion := text.findAux (· == '\n') text.rawEndPos insertion + '\n'
+  let insertion := text.findAux (· == '\n') text.endPos insertion + '\n'
   pure (path, inputCtx, header, insertion)
 
 /-- Parse a source file to extract the location of the import lines, for edits and error messages.
@@ -593,16 +593,16 @@ def main (args : List String) : IO UInt32 := do
     for stx in imports do
       let mod := decodeImport stx
       if remove.contains mod || seen.contains mod then
-        out := out ++ String.Pos.Raw.extract text pos stx.raw.getPos?.get!
+        out := out ++ text.extract pos stx.raw.getPos?.get!
         -- We use the end position of the syntax, but include whitespace up to the first newline
         pos := text.findAux (· == '\n') text.rawEndPos stx.raw.getTailPos?.get! + '\n'
       seen := seen.insert mod
-    out := out ++ String.Pos.Raw.extract text pos insertion
+    out := out ++ text.extract pos insertion
     for mod in add do
       if !seen.contains mod then
         seen := seen.insert mod
         out := out ++ s!"{mod}\n"
-    out := out ++ String.Pos.Raw.extract text insertion text.rawEndPos
+    out := out ++ text.extract insertion text.rawEndPos
 
     IO.FS.writeFile path out
     count := count + 1

script/bench.sh

@@ -0,0 +1,96 @@
+#!/usr/bin/env bash
+set -euxo pipefail
+
+cmake --preset release 1>&2
+
+# We benchmark against stage2/bin to test new optimizations.
+timeout -s KILL 1h time make -C build/release -j$(nproc) stage3 1>&2
+export PATH=$PWD/build/release/stage2/bin:$PATH
+
+# The extra opts used to be passed to the Makefile during benchmarking only but with Lake it is
+# easier to configure them statically.
+cmake -B build/release/stage3 -S src -DLEAN_EXTRA_LAKEFILE_TOML='weakLeanArgs=["-Dprofiler=true", "-Dprofiler.threshold=9999999", "--stats"]' 1>&2
+
+(
+cd tests/bench
+timeout -s KILL 1h time temci exec --config speedcenter.yaml --in speedcenter.exec.velcom.yaml 1>&2
+temci report run_output.yaml --reporter codespeed2
+)
+
+if [ -d .git ]; then
+    DIR="$(git rev-parse @)"
+    BASE_URL="https://speed.lean-lang.org/lean4-out/$DIR"
+    {
+        cat <<'EOF'
+<!DOCTYPE html>
+<html>
+<head>
+  <meta charset="UTF-8">
+  <title>Lakeprof Report</title>
+</head>
+<h1>Lakeprof Report</h1>
+<button type="button" id="btn_fetch">View build trace in Perfetto</button>
+<script type="text/javascript">
+const ORIGIN = 'https://ui.perfetto.dev';
+
+const btnFetch = document.getElementById('btn_fetch');
+
+async function fetchAndOpen(traceUrl) {
+  const resp = await fetch(traceUrl);
+  // Error checking is left as an exercise to the reader.
+  const blob = await resp.blob();
+  const arrayBuffer = await blob.arrayBuffer();
+  openTrace(arrayBuffer, traceUrl);
+}
+
+function openTrace(arrayBuffer, traceUrl) {
+  const win = window.open(ORIGIN);
+  if (!win) {
+    btnFetch.style.background = '#f3ca63';
+  	btnFetch.onclick = () => openTrace(arrayBuffer);
+    btnFetch.innerText = 'Popups blocked, click here to open the trace file';
+    return;
+  }
+
+  const timer = setInterval(() => win.postMessage('PING', ORIGIN), 50);
+
+  const onMessageHandler = (evt) => {
+    if (evt.data !== 'PONG') return;
+
+    // We got a PONG, the UI is ready.
+    window.clearInterval(timer);
+    window.removeEventListener('message', onMessageHandler);
+
+    const reopenUrl = new URL(location.href);
+    reopenUrl.hash = `#reopen=${traceUrl}`;
+    win.postMessage({
+      perfetto: {
+        buffer: arrayBuffer,
+        title: 'Lake Build Trace',
+        url: reopenUrl.toString(),
+    }}, ORIGIN);
+  };
+
+  window.addEventListener('message', onMessageHandler);
+}
+
+// This is triggered when following the link from the Perfetto UI's sidebar.
+if (location.hash.startsWith('#reopen=')) {
+ const traceUrl = location.hash.substr(8);
+ fetchAndOpen(traceUrl);
+}
+EOF
+        cat <<EOF
+btnFetch.onclick = () => fetchAndOpen("$BASE_URL/lakeprof.trace_event");
+</script>
+EOF
+        echo "<pre><code>"
+        (cd src; lakeprof report -prc)
+        echo "</code></pre>"
+        echo "</body></html>"
+    } | tee index.html
+
+    curl -T index.html $BASE_URL/index.html
+    curl -T src/lakeprof.log $BASE_URL/lakeprof.log
+    curl -T src/lakeprof.trace_event $BASE_URL/lakeprof.trace_event
+fi

script/prepare-llvm-linux.sh

@@ -58,11 +58,7 @@ OPTIONS=()
 # We build cadical using the custom toolchain on Linux to avoid glibc versioning issues
 echo -n " -DLEAN_STANDALONE=ON -DCADICAL_USE_CUSTOM_CXX=ON"
 echo -n " -DCMAKE_CXX_COMPILER=$PWD/llvm-host/bin/clang++ -DLEAN_CXX_STDLIB='-Wl,-Bstatic -lc++ -lc++abi -Wl,-Bdynamic'"
-# these should also be used for cadical, so do not use `LEAN_EXTRA_CXX_FLAGS` here
-echo -n " -DCMAKE_CXX_FLAGS='--sysroot $PWD/llvm -idirafter $GLIBC_DEV/include ${EXTRA_FLAGS:-}'"
-# the above does not include linker flags which will be added below based on context, so skip the
-# generic check by cmake
-echo -n " -DCMAKE_C_COMPILER_WORKS=1 -DCMAKE_CXX_COMPILER_WORKS=1"
+echo -n " -DLEAN_EXTRA_CXX_FLAGS='--sysroot $PWD/llvm -idirafter $GLIBC_DEV/include ${EXTRA_FLAGS:-}'"
 # use target compiler directly when not cross-compiling
 if [[ -L llvm-host ]]; then
   echo -n " -DCMAKE_C_COMPILER=$PWD/stage1/bin/clang"

script/release_checklist.py

@@ -31,8 +31,6 @@ What this script does:
    - Ensures tags are merged into stable branches (for non-RC releases)
    - Verifies bump branches exist and are configured correctly
    - Special handling for ProofWidgets4 release tags
-   - For mathlib4: runs verify_version_tags.py to validate the release tag
-     (checks git/GitHub consistency, toolchain, elan, cache, and build)
 
 3. Optionally automates missing steps (when not in --dry-run mode):
    - Creates missing release tags using push_repo_release_tag.py
@@ -501,57 +499,6 @@ def check_proofwidgets4_release(repo_url, target_toolchain, github_token):
     print(f"     You will need to create and push a tag v0.0.{next_version}")
     return False
 
-def run_mathlib_verify_version_tags(toolchain, verbose=False):
-    """Run mathlib4's verify_version_tags.py script to validate the release tag.
-
-    This clones mathlib4 to a temp directory and runs the verification script.
-    Returns True if verification passes, False otherwise.
-    """
-    import tempfile
-
-    print(f"  ... Running mathlib4 verify_version_tags.py {toolchain}")
-
-    with tempfile.TemporaryDirectory() as tmpdir:
-        # Clone mathlib4 (shallow clone is sufficient for running the script)
-        clone_result = subprocess.run(
-            ['git', 'clone', '--depth', '1', 'https://github.com/leanprover-community/mathlib4.git', tmpdir],
-            capture_output=True,
-            text=True
-        )
-        if clone_result.returncode != 0:
-            print(f"  ❌ Failed to clone mathlib4: {clone_result.stderr.strip()[:200]}")
-            return False
-
-        # Run the verification script
-        script_path = os.path.join(tmpdir, 'scripts', 'verify_version_tags.py')
-        if not os.path.exists(script_path):
-            print(f"  ❌ verify_version_tags.py not found in mathlib4 (expected at scripts/verify_version_tags.py)")
-            return False
-
-        # Run from the mathlib4 directory so git operations work
-        result = subprocess.run(
-            ['python3', script_path, toolchain],
-            cwd=tmpdir,
-            capture_output=True,
-            text=True,
-            timeout=900  # 15 minutes timeout for cache download etc.
-        )
-
-        # Print output with indentation
-        if result.stdout:
-            for line in result.stdout.strip().split('\n'):
-                print(f"     {line}")
-        if result.stderr:
-            for line in result.stderr.strip().split('\n'):
-                print(f"     {line}")
-
-        if result.returncode != 0:
-            print(f"  ❌ mathlib4 verify_version_tags.py failed")
-            return False
-
-        print(f"  ✅ mathlib4 verify_version_tags.py passed")
-        return True
-
 def main():
     parser = argparse.ArgumentParser(description="Check release status of Lean4 repositories")
     parser.add_argument("toolchain", help="The toolchain version to check (e.g., v4.6.0)")
@@ -816,12 +763,6 @@ def main():
                 repo_status[name] = False
                 continue
 
-        # For mathlib4, run verify_version_tags.py to validate the release tag
-        if name == "mathlib4":
-            if not run_mathlib_verify_version_tags(toolchain, verbose):
-                repo_status[name] = False
-                continue
-
         repo_status[name] = success
 
     # Final check for lean4 master branch

src/CMakeLists.txt

@@ -42,7 +42,7 @@ if(LLD_PATH)
 endif()
 
 set(LEAN_EXTRA_LINKER_FLAGS ${LEAN_EXTRA_LINKER_FLAGS_DEFAULT} CACHE STRING "Additional flags used by the linker")
-set(LEAN_EXTRA_CXX_FLAGS "" CACHE STRING "Additional flags used by the C++ compiler. Unlike `CMAKE_CXX_FLAGS`, these will not be used to build e.g. cadical.")
+set(LEAN_EXTRA_CXX_FLAGS "" CACHE STRING "Additional flags used by the C++ compiler")
 set(LEAN_TEST_VARS "LEAN_CC=${CMAKE_C_COMPILER}" CACHE STRING "Additional environment variables used when running tests")
 
 if (NOT CMAKE_BUILD_TYPE)
@@ -191,7 +191,7 @@ endif()
 set(CMAKE_MODULE_PATH ${CMAKE_MODULE_PATH} "${CMAKE_SOURCE_DIR}/cmake/Modules")
 
 # Initialize CXXFLAGS.
-set(CMAKE_CXX_FLAGS                "${CMAKE_CXX_FLAGS} ${LEAN_EXTRA_CXX_FLAGS} -DLEAN_BUILD_TYPE=\"${CMAKE_BUILD_TYPE}\" -DLEAN_EXPORTING")
+set(CMAKE_CXX_FLAGS                "${LEAN_EXTRA_CXX_FLAGS} -DLEAN_BUILD_TYPE=\"${CMAKE_BUILD_TYPE}\" -DLEAN_EXPORTING")
 set(CMAKE_CXX_FLAGS_DEBUG          "-DLEAN_DEBUG")
 set(CMAKE_CXX_FLAGS_MINSIZEREL     "-DNDEBUG")
 set(CMAKE_CXX_FLAGS_RELEASE        "-DNDEBUG")

src/Init/Control/Basic.lean

@@ -25,7 +25,7 @@ instances are provided for the same type.
 instance (priority := 500) instForInOfForIn' [ForIn' m ρ α d] : ForIn m ρ α where
   forIn x b f := forIn' x b fun a _ => f a
 
-@[simp] theorem forIn'_eq_forIn [d : Membership α ρ] [ForIn' m ρ α d] {β} (x : ρ) (b : β)
+@[simp] theorem forIn'_eq_forIn [d : Membership α ρ] [ForIn' m ρ α d] {β} [Monad m] (x : ρ) (b : β)
     (f : (a : α) → a ∈ x → β → m (ForInStep β)) (g : (a : α) → β → m (ForInStep β))
     (h : ∀ a m b, f a m b = g a b) :
     forIn' x b f = forIn x b g := by
@@ -40,7 +40,7 @@ instance (priority := 500) instForInOfForIn' [ForIn' m ρ α d] : ForIn m ρ α
   simp [h]
   rfl
 
-@[wf_preprocess] theorem forIn_eq_forIn' [d : Membership α ρ] [ForIn' m ρ α d] {β}
+@[wf_preprocess] theorem forIn_eq_forIn' [d : Membership α ρ] [ForIn' m ρ α d] {β} [Monad m]
     (x : ρ) (b : β) (f : (a : α) → β → m (ForInStep β)) :
     forIn x b f = forIn' x b (fun x h => binderNameHint x f <| binderNameHint h () <| f x) := by
   rfl
@@ -403,7 +403,7 @@ class ForM (m : Type u → Type v) (γ : Type w₁) (α : outParam (Type w₂))
   /--
   Runs the monadic action `f` on each element of the collection `coll`.
   -/
-  forM (coll : γ) (f : α → m PUnit) : m PUnit
+  forM [Monad m] (coll : γ) (f : α → m PUnit) : m PUnit
 
 export ForM (forM)
 

src/Init/Core.lean

@@ -377,7 +377,7 @@ class ForIn (m : Type u₁ → Type u₂) (ρ : Type u) (α : outParam (Type v))
   More information about the translation of `for` loops into `ForIn.forIn` is available in [the Lean
   reference manual](lean-manual://section/monad-iteration-syntax).
   -/
-  forIn {β} (xs : ρ) (b : β) (f : α → β → m (ForInStep β)) : m β
+  forIn {β} [Monad m] (xs : ρ) (b : β) (f : α → β → m (ForInStep β)) : m β
 
 export ForIn (forIn)
 
@@ -405,7 +405,7 @@ class ForIn' (m : Type u₁ → Type u₂) (ρ : Type u) (α : outParam (Type v)
   More information about the translation of `for` loops into `ForIn'.forIn'` is available in [the
   Lean reference manual](lean-manual://section/monad-iteration-syntax).
   -/
-  forIn' {β} (x : ρ) (b : β) (f : (a : α) → a ∈ x → β → m (ForInStep β)) : m β
+  forIn' {β} [Monad m] (x : ρ) (b : β) (f : (a : α) → a ∈ x → β → m (ForInStep β)) : m β
 
 export ForIn' (forIn')
 

src/Init/Data/Array/Basic.lean

@@ -242,7 +242,7 @@ Examples:
 * `#["red", "green", "blue", "brown"].swapIfInBounds 0 4 = #["red", "green", "blue", "brown"]`
 * `#["red", "green", "blue", "brown"].swapIfInBounds 9 2 = #["red", "green", "blue", "brown"]`
 -/
-@[extern "lean_array_swap", expose]
+@[extern "lean_array_swap", grind]
 def swapIfInBounds (xs : Array α) (i j : @& Nat) : Array α :=
   if h₁ : i < xs.size then
   if h₂ : j < xs.size then swap xs i j
@@ -570,7 +570,7 @@ protected def forIn' {α : Type u} {β : Type v} {m : Type v → Type w} [Monad
       | ForInStep.yield b => loop i (Nat.le_of_lt h') b
   loop as.size (Nat.le_refl _) b
 
-instance [Monad m] : ForIn' m (Array α) α inferInstance where
+instance : ForIn' m (Array α) α inferInstance where
   forIn' := Array.forIn'
 
 -- No separate `ForIn` instance is required because it can be derived from `ForIn'`.
@@ -1001,7 +1001,7 @@ unless `start < stop`. By default, the entire array is used.
 protected def forM {α : Type u} {m : Type v → Type w} [Monad m] (f : α → m PUnit) (as : Array α) (start := 0) (stop := as.size) : m PUnit :=
   as.foldlM (fun _ => f) ⟨⟩ start stop
 
-instance [Monad m] : ForM m (Array α) α where
+instance : ForM m (Array α) α where
   forM xs f := Array.forM f xs
 
 -- We simplify `Array.forM` to `forM`.

src/Init/Data/Array/Lemmas.lean

@@ -3966,29 +3966,28 @@ theorem getElem_modify_of_ne {xs : Array α} {i : Nat} (h : i ≠ j)
 
 /-! ### swap -/
 
-@[grind =]
-theorem getElem_swap {xs : Array α} {i j : Nat} (hi hj) {k : Nat} (hk : k < (xs.swap i j hi hj).size) :
-    (xs.swap i j hi hj)[k] = if k = i then xs[j] else if k = j then xs[i] else xs[k]'(by simp_all) := by
-  simp only [swap_def, getElem_set, eq_comm (a := k)]
-  split <;> split <;> simp_all
-
 @[simp] theorem getElem_swap_right {xs : Array α} {i j : Nat} {hi hj} :
     (xs.swap i j hi hj)[j]'(by simpa using hj) = xs[i] := by
-  simp +contextual [getElem_swap]
+  simp [swap_def]
 
 @[simp] theorem getElem_swap_left {xs : Array α} {i j : Nat} {hi hj} :
     (xs.swap i j hi hj)[i]'(by simpa using hi) = xs[j] := by
-  simp [getElem_swap]
+  simp +contextual [swap_def, getElem_set]
 
-@[simp] theorem getElem_swap_of_ne {xs : Array α} {i j : Nat} {hi hj}
-    {h : k < (xs.swap i j hi hj).size} (hi' : k ≠ i) (hj' : k ≠ j) :
-    (xs.swap i j hi hj)[k] = xs[k]'(by simp_all) := by
-  simp [getElem_swap, hi', hj']
+@[simp] theorem getElem_swap_of_ne {xs : Array α} {i j : Nat} {hi hj} (hp : k < xs.size)
+    (hi' : k ≠ i) (hj' : k ≠ j) : (xs.swap i j hi hj)[k]'(xs.size_swap .. |>.symm ▸ hp) = xs[k] := by
+  simp [swap_def, getElem_set, hi'.symm, hj'.symm]
 
-@[deprecated getElem_swap (since := "2025-10-10")]
 theorem getElem_swap' {xs : Array α} {i j : Nat} {hi hj} {k : Nat} (hk : k < xs.size) :
-    (xs.swap i j hi hj)[k]'(by simp_all) = if k = i then xs[j] else if k = j then xs[i] else xs[k] :=
-  getElem_swap _ _ _
+    (xs.swap i j hi hj)[k]'(by simp_all) = if k = i then xs[j] else if k = j then xs[i] else xs[k] := by
+  split
+  · simp_all only [getElem_swap_left]
+  · split <;> simp_all
+
+@[grind =]
+theorem getElem_swap {xs : Array α} {i j : Nat} (hi hj) {k : Nat} (hk : k < (xs.swap i j hi hj).size) :
+    (xs.swap i j hi hj)[k] = if k = i then xs[j] else if k = j then xs[i] else xs[k]'(by simp_all) := by
+  apply getElem_swap'
 
 @[simp] theorem swap_swap {xs : Array α} {i j : Nat} (hi hj) :
     (xs.swap i j hi hj).swap i j ((xs.size_swap ..).symm ▸ hi) ((xs.size_swap ..).symm ▸ hj) = xs := by
@@ -4009,66 +4008,8 @@ theorem swap_comm {xs : Array α} {i j : Nat} (hi hj) : xs.swap i j hi hj = xs.s
     · split <;> simp_all
     · split <;> simp_all
 
-/-! ### swapIfInBounds -/
-
-@[grind =] theorem swapIfInBounds_def {xs : Array α} {i j : Nat} :
-    xs.swapIfInBounds i j = if h₁ : i < xs.size then
-  if h₂ : j < xs.size then swap xs i j else xs else xs := rfl
-
 @[simp, grind =] theorem size_swapIfInBounds {xs : Array α} {i j : Nat} :
-    (xs.swapIfInBounds i j).size = xs.size := by
-  unfold swapIfInBounds; split <;> (try split) <;> simp [size_swap]
-
-@[grind =] theorem getElem_swapIfInBounds {xs : Array α} {i j k : Nat}
-    (hk : k < (xs.swapIfInBounds i j).size) :
-    (xs.swapIfInBounds i j)[k] =
-    if h₁ : k = i ∧ j < xs.size then xs[j]'h₁.2 else if h₂ : k = j ∧ i < xs.size then xs[i]'h₂.2
-    else xs[k]'(by simp_all) := by
-  rw [size_swapIfInBounds] at hk
-  unfold swapIfInBounds
-  split <;> rename_i hi
-  · split <;> rename_i hj
-    · simp only [hi, hj, and_true]
-      exact getElem_swap _ _ _
-    · simp only [hi, hj, and_true, and_false, dite_false]
-      split <;> simp_all
-  · simp only [hi, and_false, dite_false]
-    split <;> simp_all
-
-@[simp]
-theorem getElem_swapIfInBounds_of_size_le_left {xs : Array α} {i j k : Nat} (hi : xs.size ≤ i)
-    (hk : k < (xs.swapIfInBounds i j).size) :
-    (xs.swapIfInBounds i j)[k] = xs[k]'(Nat.lt_of_lt_of_eq hk size_swapIfInBounds) := by
-  have h₁ : k ≠ i := Nat.ne_of_lt <| Nat.lt_of_lt_of_le hk <|
-    Nat.le_trans (Nat.le_of_eq (size_swapIfInBounds)) hi
-  have h₂ : ¬ (i < xs.size) := Nat.not_lt_of_le hi
-  simp [getElem_swapIfInBounds, h₁, h₂]
-
-@[simp]
-theorem getElem_swapIfInBounds_of_size_le_right {xs : Array α} {i j k : Nat} (hj : xs.size ≤ j)
-    (hk : k < (xs.swapIfInBounds i j).size) :
-    (xs.swapIfInBounds i j)[k] = xs[k]'(Nat.lt_of_lt_of_eq hk size_swapIfInBounds) := by
-  have h₁ : ¬ (j < xs.size) := Nat.not_lt_of_le hj
-  have h₂ : k ≠ j := Nat.ne_of_lt <| Nat.lt_of_lt_of_le hk <|
-    Nat.le_trans (Nat.le_of_eq (size_swapIfInBounds)) hj
-  simp [getElem_swapIfInBounds, h₁, h₂]
-
-@[simp]
-theorem getElem_swapIfInBounds_left {xs : Array α} {i j : Nat} (hj : j < xs.size)
-    (hi : i < (xs.swapIfInBounds i j).size) : (xs.swapIfInBounds i j)[i] = xs[j] := by
-  simp [getElem_swapIfInBounds, hj]
-
-@[simp]
-theorem getElem_swapIfInBounds_right {xs : Array α} {i j : Nat} (hi : i < xs.size)
-    (hj : j < (xs.swapIfInBounds i j).size) :
-    (xs.swapIfInBounds i j)[j] = xs[i] := by
-  simp +contextual [getElem_swapIfInBounds, hi]
-
-@[simp]
-theorem getElem_swapIfInBounds_of_ne_of_ne {xs : Array α} {i j k : Nat} (hi : k ≠ i) (hj : k ≠ j)
-    (hk : k < (xs.swapIfInBounds i j).size) :
-    (xs.swapIfInBounds i j)[k] = xs[k]'(Nat.lt_of_lt_of_eq hk size_swapIfInBounds) := by
-  simp [getElem_swapIfInBounds, hi, hj]
+    (xs.swapIfInBounds i j).size = xs.size := by unfold swapIfInBounds; split <;> (try split) <;> simp [size_swap]
 
 /-! ### swapAt -/
 

src/Init/Data/ByteArray/Basic.lean

@@ -132,11 +132,6 @@ Copies the bytes with indices {name}`b` (inclusive) to {name}`e` (exclusive) to
 def extract (a : ByteArray) (b e : Nat) : ByteArray :=
   a.copySlice b empty 0 (e - b)
 
-/--
-Appends two byte arrays using fast array primitives instead of converting them into lists and back.
-
-In compiled code, this function replaces calls to {name}`ByteArray.append`.
--/
 @[inline]
 protected def fastAppend (a : ByteArray) (b : ByteArray) : ByteArray :=
   -- we assume that `append`s may be repeated, so use asymptotic growing; use `copySlice` directly to customize
@@ -248,7 +243,7 @@ protected def forIn {β : Type v} {m : Type v → Type w} [Monad m] (as : ByteAr
       | ForInStep.yield b => loop i (Nat.le_of_lt h') b
   loop as.size (Nat.le_refl _) b
 
-instance [Monad m] : ForIn m ByteArray UInt8 where
+instance : ForIn m ByteArray UInt8 where
   forIn := ByteArray.forIn
 
 /--

src/Init/Data/FloatArray/Basic.lean

@@ -129,7 +129,7 @@ protected def forIn {β : Type v} {m : Type v → Type w} [Monad m] (as : FloatA
       | ForInStep.yield b => loop i (Nat.le_of_lt h') b
   loop as.size (Nat.le_refl _) b
 
-instance [Monad m] : ForIn m FloatArray Float where
+instance : ForIn m FloatArray Float where
   forIn := FloatArray.forIn
 
 /-- See comment at `forInUnsafe` -/

src/Init/Data/Int/DivMod/Lemmas.lean

@@ -1781,16 +1781,6 @@ theorem ediv_lt_ediv_iff_of_dvd_of_neg_of_neg {a b c d : Int} (hb : b < 0) (hd :
   obtain ⟨⟨x, rfl⟩, y, rfl⟩ := hba, hdc
   simp [*, Int.ne_of_lt, d.mul_assoc, b.mul_comm]
 
-theorem ediv_lt_ediv_of_lt {a b c : Int} (h : a < b) (hcb : c ∣ b) (hc : 0 < c) :
-    a / c < b / c :=
-  Int.lt_ediv_of_mul_lt (Int.le_of_lt hc) hcb 
-    (Int.lt_of_le_of_lt (Int.ediv_mul_le _ (Int.ne_of_gt hc)) h)
-  
-theorem ediv_lt_ediv_of_lt_of_neg {a b c : Int} (h : b < a) (hca : c ∣ a) (hc : c < 0) :
-    a / c < b / c :=
-  (Int.ediv_lt_iff_of_dvd_of_neg hc hca).2 
-    (Int.lt_of_le_of_lt (Int.mul_ediv_self_le (Int.ne_of_lt hc)) h)
-
 /-! ### `tdiv` and ordering -/
 
 -- Theorems about `tdiv` and ordering, whose `ediv` analogues are in `Bootstrap.lean`.

src/Init/Data/Int/Order.lean

@@ -377,15 +377,6 @@ protected theorem le_iff_lt_add_one {a b : Int} : a ≤ b ↔ a < b + 1 := by
 
 @[grind =] protected theorem max_def (n m : Int) : max n m = if n ≤ m then m else n := rfl
 
-end Int
-namespace Lean.Meta.Grind.Lia
-
-scoped grind_pattern Int.min_def => min n m
-scoped grind_pattern Int.max_def => max n m
-
-end Lean.Meta.Grind.Lia
-namespace Int
-
 @[simp] protected theorem neg_min_neg (a b : Int) : min (-a) (-b) = -max a b := by
   rw [Int.min_def, Int.max_def]
   simp

src/Init/Data/Iterators/Basic.lean

@@ -678,7 +678,6 @@ Given this typeclass, termination proofs for well-founded recursion over an iter
 `it.finitelyManySteps` as a termination measure.
 -/
 class Finite (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] : Prop where
-  /-- The relation of plausible successors is well-founded. -/
   wf : WellFounded (IterM.IsPlausibleSuccessorOf (α := α) (m := m))
 
 theorem Finite.wf_of_id {α : Type w} {β : Type w} [Iterator α Id β] [Finite α Id] :
@@ -798,7 +797,6 @@ Given this typeclass, termination proofs for well-founded recursion over an iter
 `it.finitelyManySkips` as a termination measure.
 -/
 class Productive (α m) {β} [Iterator α m β] : Prop where
-  /-- The relation of plausible successors during skips is well-founded. -/
   wf : WellFounded (IterM.IsPlausibleSkipSuccessorOf (α := α) (m := m))
 
 /--

src/Init/Data/Iterators/Consumers/Loop.lean

@@ -9,8 +9,6 @@ prelude
 public import Init.Data.Iterators.Consumers.Collect
 public import Init.Data.Iterators.Consumers.Monadic.Loop
 
-set_option linter.missingDocs true
-
 public section
 
 /-!
@@ -48,9 +46,6 @@ instance (α : Type w) (β : Type w) (n : Type x → Type x') [Monad n]
   haveI : ForIn' n (Iter (α := α) β) β _ := Iter.instForIn'
   instForInOfForIn'
 
-/--
-An implementation of `for h : ... in ... do ...` notation for partial iterators.
--/
 @[always_inline, inline]
 def Iter.Partial.instForIn' {α : Type w} {β : Type w} {n : Type x → Type x'} [Monad n]
     [Iterator α Id β] [IteratorLoopPartial α Id n] :
@@ -68,12 +63,12 @@ instance (α : Type w) (β : Type w) (n : Type x → Type x') [Monad n]
   instForInOfForIn'
 
 instance {m : Type x → Type x'}
-    {α : Type w} {β : Type w} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id m] [Monad m] :
+    {α : Type w} {β : Type w} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id m] :
     ForM m (Iter (α := α) β) β where
   forM it f := forIn it PUnit.unit (fun out _ => do f out; return .yield .unit)
 
 instance {m : Type x → Type x'}
-    {α : Type w} {β : Type w} [Iterator α Id β] [Finite α Id] [IteratorLoopPartial α Id m] [Monad m] :
+    {α : Type w} {β : Type w} [Iterator α Id β] [Finite α Id] [IteratorLoopPartial α Id m] :
     ForM m (Iter.Partial (α := α) β) β where
   forM it f := forIn it PUnit.unit (fun out _ => do f out; return .yield .unit)
 
@@ -207,11 +202,6 @@ def Iter.all {α β : Type w}
     (p : β → Bool) (it : Iter (α := α) β) : Bool :=
   (it.allM (fun x => pure (f := Id) (p x))).run
 
-/--
-Steps through the iterator until the monadic function `f` returns `some` for an element, at which
-point iteration stops and the result of `f` is returned. If the iterator is completely consumed
-without `f` returning `some`, then the result is `none`.
--/
 @[inline]
 def Iter.findSomeM? {α β : Type w} {γ : Type x} {m : Type x → Type w'} [Monad m] [Iterator α Id β]
     [IteratorLoop α Id m] [Finite α Id] (it : Iter (α := α) β) (f : β → m (Option γ)) :
@@ -221,7 +211,7 @@ def Iter.findSomeM? {α β : Type w} {γ : Type x} {m : Type x → Type w'} [Mon
     | none => return .yield none
     | some fx => return .done (some fx))
 
-@[inline, inherit_doc Iter.findSomeM?]
+@[inline]
 def Iter.Partial.findSomeM? {α β : Type w} {γ : Type x} {m : Type x → Type w'} [Monad m]
     [Iterator α Id β] [IteratorLoopPartial α Id m] (it : Iter.Partial (α := α) β)
     (f : β → m (Option γ)) :
@@ -231,50 +221,36 @@ def Iter.Partial.findSomeM? {α β : Type w} {γ : Type x} {m : Type x → Type
     | none => return .yield none
     | some fx => return .done (some fx))
 
-/--
-Steps through the iterator until `f` returns `some` for an element, at which point iteration stops
-and the result of `f` is returned. If the iterator is completely consumed without `f` returning
-`some`, then the result is `none`.
--/
 @[inline]
 def Iter.findSome? {α β : Type w} {γ : Type x} [Iterator α Id β]
     [IteratorLoop α Id Id] [Finite α Id] (it : Iter (α := α) β) (f : β → Option γ) :
     Option γ :=
   Id.run (it.findSomeM? (pure <| f ·))
 
-@[inline, inherit_doc Iter.findSome?]
+@[inline]
 def Iter.Partial.findSome? {α β : Type w} {γ : Type x} [Iterator α Id β]
     [IteratorLoopPartial α Id Id] (it : Iter.Partial (α := α) β) (f : β → Option γ) :
     Option γ :=
   Id.run (it.findSomeM? (pure <| f ·))
 
-/--
-Steps through the iterator until an element satisfies the monadic predicate `f`, at which point
-iteration stops and the element is returned. If no element satisfies `f`, then the result is
-`none`.
--/
 @[inline]
 def Iter.findM? {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α Id β]
     [IteratorLoop α Id m] [Finite α Id] (it : Iter (α := α) β) (f : β → m (ULift Bool)) :
     m (Option β) :=
   it.findSomeM? (fun x => return if (← f x).down then some x else none)
 
-@[inline, inherit_doc Iter.findM?]
+@[inline]
 def Iter.Partial.findM? {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α Id β]
     [IteratorLoopPartial α Id m] (it : Iter.Partial (α := α) β) (f : β → m (ULift Bool)) :
     m (Option β) :=
   it.findSomeM? (fun x => return if (← f x).down then some x else none)
 
-/--
-Steps through the iterator until an element satisfies `f`, at which point iteration stops and the
-element is returned. If no element satisfies `f`, then the result is `none`.
--/
 @[inline]
 def Iter.find? {α β : Type w} [Iterator α Id β] [IteratorLoop α Id Id]
     [Finite α Id] (it : Iter (α := α) β) (f : β → Bool) : Option β :=
   Id.run (it.findM? (pure <| .up <| f ·))
 
-@[inline, inherit_doc Iter.find?]
+@[inline]
 def Iter.Partial.find? {α β : Type w} [Iterator α Id β] [IteratorLoopPartial α Id Id]
     (it : Iter.Partial (α := α) β) (f : β → Bool) : Option β :=
   Id.run (it.findM? (pure <| .up <| f ·))

src/Init/Data/Iterators/Consumers/Monadic/Loop.lean

@@ -247,10 +247,10 @@ This `ForIn'`-style loop construct traverses a finite iterator using an `Iterato
 -/
 @[always_inline, inline]
 def IteratorLoop.finiteForIn' {m : Type w → Type w'} {n : Type x → Type x'}
-    {α : Type w} {β : Type w} [Iterator α m β] [Finite α m] [IteratorLoop α m n] [Monad n]
+    {α : Type w} {β : Type w} [Iterator α m β] [Finite α m] [IteratorLoop α m n]
     (lift : ∀ γ δ, (γ → n δ) → m γ → n δ) :
     ForIn' n (IterM (α := α) m β) β ⟨fun it out => it.IsPlausibleIndirectOutput out⟩ where
-  forIn' {γ} it init f :=
+  forIn' {γ} [Monad n] it init f :=
     IteratorLoop.forIn (α := α) (m := m) lift γ (fun _ _ _ => True)
       wellFounded_of_finite
       it init (fun out h acc => (⟨·, .intro⟩) <$> f out h acc)
@@ -288,13 +288,13 @@ instance {m : Type w → Type w'} {n : Type w → Type w''}
   instForInOfForIn'
 
 instance {m : Type w → Type w'} {n : Type w → Type w''}
-    {α : Type w} {β : Type w} [Iterator α m β] [Finite α m] [IteratorLoop α m n] [Monad n]
+    {α : Type w} {β : Type w} [Iterator α m β] [Finite α m] [IteratorLoop α m n]
     [MonadLiftT m n] :
     ForM n (IterM (α := α) m β) β where
   forM it f := forIn it PUnit.unit (fun out _ => do f out; return .yield .unit)
 
 instance {m : Type w → Type w'} {n : Type w → Type w''}
-    {α : Type w} {β : Type w} [Iterator α m β] [IteratorLoopPartial α m n] [Monad n]
+    {α : Type w} {β : Type w} [Iterator α m β] [IteratorLoopPartial α m n]
     [MonadLiftT m n] :
     ForM n (IterM.Partial (α := α) m β) β where
   forM it f := forIn it PUnit.unit (fun out _ => do f out; return .yield .unit)

src/Init/Data/List/Control.lean

@@ -471,7 +471,7 @@ theorem findM?_eq_findSomeM? [Monad m] [LawfulMonad m] {p : α → m Bool} {as :
         loop as' b this
   loop as init ⟨[], rfl⟩
 
-instance [Monad m] : ForIn' m (List α) α inferInstance where
+instance : ForIn' m (List α) α inferInstance where
   forIn' := List.forIn'
 
 -- No separate `ForIn` instance is required because it can be derived from `ForIn'`.
@@ -485,7 +485,7 @@ instance [Monad m] : ForIn' m (List α) α inferInstance where
 @[simp, grind =] theorem forIn_nil [Monad m] {f : α → β → m (ForInStep β)} {b : β} : forIn [] b f = pure b :=
   rfl
 
-instance [Monad m] : ForM m (List α) α where
+instance : ForM m (List α) α where
   forM := List.forM
 
 -- We simplify `List.forM` to `forM`.

src/Init/Data/List/Lemmas.lean

@@ -15,7 +15,8 @@ import all Init.Data.List.Control
 public import Init.BinderPredicates
 import Init.Grind.Annotated
 
-grind_annotated "2025-01-24"
+-- TODO: turn this on after an update-stage0
+-- grind_annotated "2025-01-24"
 
 public section
 

src/Init/Data/Option/Instances.lean

@@ -168,10 +168,10 @@ Examples:
   | none  , _ => pure ⟨⟩
   | some a, f => f a
 
-instance [Monad m] : ForM m (Option α) α :=
+instance : ForM m (Option α) α :=
   ⟨Option.forM⟩
 
-instance [Monad m] : ForIn' m (Option α) α inferInstance where
+instance : ForIn' m (Option α) α inferInstance where
   forIn' x init f := do
     match x with
     | none => return init

src/Init/Data/Ord/Basic.lean

@@ -631,7 +631,7 @@ instance [Ord α] : DecidableRel (@LT.lt α ltOfOrd) := fun a b =>
   decidable_of_bool (compare a b).isLT Ordering.isLT_iff_eq_lt
 
 /--
-Constructs an `LE` instance from an `Ord` instance that asserts that the result of `compare`
+Constructs an `LT` instance from an `Ord` instance that asserts that the result of `compare`
 satisfies `Ordering.isLE`.
 -/
 @[expose] def leOfOrd [Ord α] : LE α where

src/Init/Data/Range/Basic.lean

@@ -43,7 +43,7 @@ universe u v
   have := range.step_pos
   loop init range.start (by simp)
 
-instance [Monad m] : ForIn' m Range Nat inferInstance where
+instance : ForIn' m Range Nat inferInstance where
   forIn' := Range.forIn'
 
 -- No separate `ForIn` instance is required because it can be derived from `ForIn'`.
@@ -59,7 +59,7 @@ instance [Monad m] : ForIn' m Range Nat inferInstance where
   have := range.step_pos
   loop range.start
 
-instance [Monad m] : ForM m Range Nat where
+instance : ForM m Range Nat where
   forM := Range.forM
 
 syntax:max "[" withoutPosition(":" term) "]" : term

src/Init/Data/Range/Polymorphic/PRange.lean

@@ -9,7 +9,6 @@ prelude
 public import Init.Data.Range.Polymorphic.UpwardEnumerable
 
 set_option doc.verso true
-set_option linter.missingDocs true
 
 public section
 
@@ -24,13 +23,7 @@ A range of elements of {given}`α` with closed lower and upper bounds.
 equal to {given}`b : α`. This is notation for {lean}`Rcc.mk a b`.
 -/
 structure Rcc (α : Type u) where
-  /--
-  The lower bound of the range. {name (full := Rcc.lower)}`lower` is included in the range.
-  -/
   lower : α
-  /--
-  The upper bound of the range. {name (full := Rcc.upper)}`upper` is included in the range.
-  -/
   upper : α
 
 /--
@@ -40,13 +33,7 @@ A range of elements of {given}`α` with a closed lower bound and an open upper b
 less than {given}`b : α`. This is notation for {lean}`Rco.mk a b`.
 -/
 structure Rco (α : Type u) where
-  /--
-  The lower bound of the range. {name (full := Rco.lower)}`lower` is included in the range.
-  -/
   lower : α
-  /--
-  The upper bound of the range. {name (full := Rco.upper)}`upper` is not included in the range.
-  -/
   upper : α
 
 /--
@@ -56,9 +43,6 @@ An upward-unbounded range of elements of {given}`α` with a closed lower bound.
 This is notation for {lean}`Rci.mk a`.
 -/
 structure Rci (α : Type u) where
-  /--
-  The lower bound of the range. {name (full := Rci.lower)}`lower` is included in the range.
-  -/
   lower : α
 
 /--
@@ -68,13 +52,7 @@ A range of elements of {given}`α` with an open lower bound and a closed upper b
 {given}`b : α`. This is notation for {lean}`Roc.mk a b`.
 -/
 structure Roc (α : Type u) where
-  /--
-  The lower bound of the range. {name (full := Roc.lower)}`lower` is not included in the range.
-  -/
   lower : α
-  /--
-  The upper bound of the range. {name (full := Roc.upper)}`upper` is included in the range.
-  -/
   upper : α
 
 /--
@@ -84,13 +62,7 @@ A range of elements of {given}`α` with an open lower and upper bounds.
 {given}`b : α`. This is notation for {lean}`Roo.mk a b`.
 -/
 structure Roo (α : Type u) where
-  /--
-  The lower bound of the range. {name (full := Roo.lower)}`lower` is not included in the range.
-  -/
   lower : α
-  /--
-  The upper bound of the range. {name (full := Roo.upper)}`upper` is not included in the range.
-  -/
   upper : α
 
 /--
@@ -100,9 +72,6 @@ An upward-unbounded range of elements of {given}`α` with an open lower bound.
 This is notation for {lean}`Roi.mk a`.
 -/
 structure Roi (α : Type u) where
-  /--
-  The lower bound of the range. {name (full := Roi.lower)}`lower` is not included in the range.
-  -/
   lower : α
 
 /--
@@ -112,9 +81,6 @@ A downward-unbounded range of elements of {given}`α` with a closed upper bound.
 This is notation for {lean}`Ric.mk b`.
 -/
 structure Ric (α : Type u) where
-  /--
-  The upper bound of the range. {name (full := Ric.upper)}`upper` is included in the range.
-  -/
   upper : α
 
 /--
@@ -124,9 +90,6 @@ A downward-unbounded range of elements of {given}`α` with an open upper bound.
 This is notation for {lean}`Rio.mk b`.
 -/
 structure Rio (α : Type u) where
-  /--
-  The upper bound of the range. {name (full := Rio.upper)}`upper` is not included in the range.
-  -/
   upper : α
 
 /--
@@ -199,10 +162,6 @@ This is a prerequisite for many functions and instances, such as
 {name (scope := "Init.Data.Range.Polymorphic.Iterators")}`Rcc.toList` or {name}`ForIn'`.
 -/
 class Rxc.IsAlwaysFinite (α : Type u) [UpwardEnumerable α] [LE α] : Prop where
-  /--
-  For every pair of elements {name}`init` and {name}`hi`, there exists a chain of successors that
-  results in an element that either has no successors or is greater than {name}`hi`.
-  -/
   finite (init : α) (hi : α) :
     ∃ n, (UpwardEnumerable.succMany? n init).elim True (¬ · ≤ hi)
 
@@ -213,10 +172,6 @@ This is a prerequisite for many functions and instances, such as
 {name (scope := "Init.Data.Range.Polymorphic.Iterators")}`Rco.toList` or {name}`ForIn'`.
 -/
 class Rxo.IsAlwaysFinite (α : Type u) [UpwardEnumerable α] [LT α] : Prop where
-  /--
-  For every pair of elements {name}`init` and {name}`hi`, there exists a chain of successors that
-  results in an element that either has no successors or is greater than {name}`hi`.
-  -/
   finite (init : α) (hi : α) :
     ∃ n, (UpwardEnumerable.succMany? n init).elim True (¬ · < hi)
 
@@ -227,10 +182,6 @@ This is a prerequisite for many functions and instances, such as
 {name (scope := "Init.Data.Range.Polymorphic.Iterators")}`Rci.toList` or {name}`ForIn'`.
 -/
 class Rxi.IsAlwaysFinite (α : Type u) [UpwardEnumerable α] : Prop where
-  /--
-  For every elements {name}`init`, there exists a chain of successors that
-  results in an element that has no successors.
-  -/
   finite (init : α) : ∃ n, UpwardEnumerable.succMany? n init = none
 
 namespace Rcc
@@ -340,7 +291,6 @@ This type class allows taking the intersection of a closed range with a
 left-closed right-open range, resulting in another left-closed right-open range.
 -/
 class Rcc.HasRcoIntersection (α : Type w) where
-  /-- The intersection operator. -/
   intersection : Rcc α → Rco α → Rco α
 
 /--
@@ -349,9 +299,6 @@ of two ranges contains exactly those elements that are contained in both ranges.
 -/
 class Rcc.LawfulRcoIntersection (α : Type w) [LT α] [LE α]
     [HasRcoIntersection α] where
-  /--
-  Every element of the intersection is an element of both original ranges.
-  -/
   mem_intersection_iff {a : α} {r : Rcc α} {s : Rco α} :
     a ∈ HasRcoIntersection.intersection r s ↔ a ∈ r ∧ a ∈ s
 
@@ -360,7 +307,6 @@ This type class allows taking the intersection of two left-closed right-open ran
 another left-closed right-open range.
 -/
 class Rco.HasRcoIntersection (α : Type w) where
-  /-- The intersection operator. -/
   intersection : Rco α → Rco α → Rco α
 
 /--
@@ -369,9 +315,6 @@ of two ranges contains exactly those elements that are contained in both ranges.
 -/
 class Rco.LawfulRcoIntersection (α : Type w) [LT α] [LE α]
     [HasRcoIntersection α] where
-  /--
-  Every element of the intersection is an element of both original ranges.
-  -/
   mem_intersection_iff {a : α} {r : Rco α} {s : Rco α} :
     a ∈ HasRcoIntersection.intersection r s ↔ a ∈ r ∧ a ∈ s
 
@@ -380,7 +323,6 @@ This type class allows taking the intersection of a left-closed right-unbounded
 left-closed right-open range, resulting in another left-closed right-open range.
 -/
 class Rci.HasRcoIntersection (α : Type w) where
-  /-- The intersection operator. -/
   intersection : Rci α → Rco α → Rco α
 
 /--
@@ -389,9 +331,6 @@ of two ranges contains exactly those elements that are contained in both ranges.
 -/
 class Rci.LawfulRcoIntersection (α : Type w) [LT α] [LE α]
     [HasRcoIntersection α] where
-  /--
-  Every element of the intersection is an element of both original ranges.
-  -/
   mem_intersection_iff {a : α} {r : Rci α} {s : Rco α} :
     a ∈ HasRcoIntersection.intersection r s ↔ a ∈ r ∧ a ∈ s
 
@@ -400,7 +339,6 @@ This type class allows taking the intersection of a left-open right-closed range
 left-closed right-open range, resulting in another left-closed right-open range.
 -/
 class Roc.HasRcoIntersection (α : Type w) where
-  /-- The intersection operator. -/
   intersection : Roc α → Rco α → Rco α
 
 /--
@@ -409,9 +347,6 @@ of two ranges contains exactly those elements that are contained in both ranges.
 -/
 class Roc.LawfulRcoIntersection (α : Type w) [LT α] [LE α]
     [HasRcoIntersection α] where
-  /--
-  Every element of the intersection is an element of both original ranges.
-  -/
   mem_intersection_iff {a : α} {r : Roc α} {s : Rco α} :
     a ∈ HasRcoIntersection.intersection r s ↔ a ∈ r ∧ a ∈ s
 
@@ -420,7 +355,6 @@ This type class allows taking the intersection of an open range with a
 left-closed right-open range, resulting in another left-closed right-open range.
 -/
 class Roo.HasRcoIntersection (α : Type w) where
-  /-- The intersection operator. -/
   intersection : Roo α → Rco α → Rco α
 
 /--
@@ -429,9 +363,6 @@ of two ranges contains exactly those elements that are contained in both ranges.
 -/
 class Roo.LawfulRcoIntersection (α : Type w) [LT α] [LE α]
     [HasRcoIntersection α] where
-  /--
-  Every element of the intersection is an element of both original ranges.
-  -/
   mem_intersection_iff {a : α} {r : Roo α} {s : Rco α} :
     a ∈ HasRcoIntersection.intersection r s ↔ a ∈ r ∧ a ∈ s
 
@@ -440,7 +371,6 @@ This type class allows taking the intersection of a left-open right-unbounded ra
 left-closed right-open range, resulting in another left-closed right-open range.
 -/
 class Roi.HasRcoIntersection (α : Type w) where
-  /-- The intersection operator. -/
   intersection : Roi α → Rco α → Rco α
 
 /--
@@ -449,9 +379,6 @@ of two ranges contains exactly those elements that are contained in both ranges.
 -/
 class Roi.LawfulRcoIntersection (α : Type w) [LT α] [LE α]
     [HasRcoIntersection α] where
-  /--
-  Every element of the intersection is an element of both original ranges.
-  -/
   mem_intersection_iff {a : α} {r : Roi α} {s : Rco α} :
     a ∈ HasRcoIntersection.intersection r s ↔ a ∈ r ∧ a ∈ s
 
@@ -460,7 +387,6 @@ This type class allows taking the intersection of a left-unbounded right-closed
 left-closed right-open range, resulting in another left-closed right-open range.
 -/
 class Ric.HasRcoIntersection (α : Type w) where
-  /-- The intersection operator. -/
   intersection : Ric α → Rco α → Rco α
 
 /--
@@ -469,9 +395,6 @@ of two ranges contains exactly those elements that are contained in both ranges.
 -/
 class Ric.LawfulRcoIntersection (α : Type w) [LT α] [LE α]
     [HasRcoIntersection α] where
-  /--
-  Every element of the intersection is an element of both original ranges.
-  -/
   mem_intersection_iff {a : α} {r : Ric α} {s : Rco α} :
     a ∈ HasRcoIntersection.intersection r s ↔ a ∈ r ∧ a ∈ s
 
@@ -480,7 +403,6 @@ This type class allows taking the intersection of a left-unbounded right-open ra
 left-closed right-open range, resulting in another left-closed right-open range.
 -/
 class Rio.HasRcoIntersection (α : Type w) where
-  /-- The intersection operator. -/
   intersection : Rio α → Rco α → Rco α
 
 /--
@@ -489,9 +411,6 @@ of two ranges contains exactly those elements that are contained in both ranges.
 -/
 class Rio.LawfulRcoIntersection (α : Type w) [LT α] [LE α]
     [HasRcoIntersection α] where
-  /--
-  Every element of the intersection is an element of both original ranges.
-  -/
   mem_intersection_iff {a : α} {r : Rio α} {s : Rco α} :
     a ∈ HasRcoIntersection.intersection r s ↔ a ∈ r ∧ a ∈ s
 

src/Init/Data/Rat/Lemmas.lean

@@ -295,15 +295,6 @@ theorem add_def (a b : Rat) :
 theorem add_def' (a b : Rat) : a + b = mkRat (a.num * b.den + b.num * a.den) (a.den * b.den) := by
   rw [add_def, normalize_eq_mkRat]
 
-theorem num_add (a b : Rat) : (a + b).num =
-    (a.num * ↑b.den + b.num * ↑a.den) /
-      ↑((a.num * ↑b.den + b.num * ↑a.den).natAbs.gcd (a.den * b.den)) := by
-  rw [add_def, num_normalize]
-
-theorem den_add (a b : Rat) : (a + b).den =
-    a.den * b.den / (a.num * ↑b.den + b.num * ↑a.den).natAbs.gcd (a.den * b.den) := by
-  rw [add_def, den_normalize]
-
 @[local simp]
 protected theorem add_zero (a : Rat) : a + 0 = a := by simp [add_def', mkRat_self]
 @[local simp]
@@ -415,13 +406,6 @@ theorem mul_def (a b : Rat) :
 theorem mul_def' (a b : Rat) : a * b = mkRat (a.num * b.num) (a.den * b.den) := by
   rw [mul_def, normalize_eq_mkRat]
 
-theorem num_mul (a b : Rat) :
-    (a * b).num = a.num * b.num / ↑((a.num * b.num).natAbs.gcd (a.den * b.den)) := by
-  rw [mul_def, num_normalize]
-theorem den_mul (a b : Rat) :
-    (a * b).den = a.den * b.den / (a.num * b.num).natAbs.gcd (a.den * b.den) := by
-  rw [mul_def, den_normalize]
-
 protected theorem mul_comm (a b : Rat) : a * b = b * a := by
   simp [mul_def, normalize_eq_mkRat, Int.mul_comm, Nat.mul_comm]
 

src/Init/Data/Slice/List/Iterator.lean

@@ -37,7 +37,7 @@ instance : SliceSize (Internal.ListSliceData α) where
   size s := (Internal.iter s).count
 
 @[no_expose]
-instance {α : Type u} {m : Type v → Type w} [Monad m] :
+instance {α : Type u} {m : Type v → Type w} :
     ForIn m (ListSlice α) α where
   forIn xs init f := forIn (Internal.iter xs) init f
 

src/Init/Data/Slice/Operations.lean

@@ -75,7 +75,7 @@ def toListRev [ToIterator (Slice γ) Id α β] [Iterator α Id β]
     [Finite α Id] (s : Slice γ) : List β :=
   Internal.iter s |>.toListRev
 
-instance {γ : Type u} {β : Type v} [Monad m] [ToIterator (Slice γ) Id α β]
+instance {γ : Type u} {β : Type v} [ToIterator (Slice γ) Id α β]
     [Iterator α Id β]
     [IteratorLoop α Id m]
     [Finite α Id] :

src/Init/Data/Stream.lean

@@ -66,7 +66,7 @@ protected partial def Stream.forIn [Stream ρ α] [Monad m] (s : ρ) (b : β) (f
     | none => return b
   visit s b
 
-instance (priority := low) [Monad m] [Stream ρ α] : ForIn m ρ α where
+instance (priority := low) [Stream ρ α] : ForIn m ρ α where
   forIn := Stream.forIn
 
 instance : ToStream (List α) (List α) where

src/Init/Data/String.lean

@@ -13,6 +13,7 @@ public import Init.Data.String.Defs
 public import Init.Data.String.Extra
 public import Init.Data.String.Iterator
 public import Init.Data.String.Lemmas
+public import Init.Data.String.Repr
 public import Init.Data.String.Bootstrap
 public import Init.Data.String.Slice
 public import Init.Data.String.Pattern
@@ -25,4 +26,3 @@ public import Init.Data.String.Termination
 public import Init.Data.String.ToSlice
 public import Init.Data.String.Search
 public import Init.Data.String.Legacy
-public import Init.Data.String.Grind

src/Init/Data/String/Bootstrap.lean

@@ -13,6 +13,9 @@ public section
 
 namespace String
 
+@[deprecated Pos.Raw (since := "2025-09-30")]
+abbrev Pos := Pos.Raw
+
 instance : OfNat String.Pos.Raw (nat_lit 0) where
   ofNat := {}
 

src/Init/Data/String/Defs.lean

@@ -74,11 +74,11 @@ Encodes a string in UTF-8 as an array of bytes.
 -/
 @[extern "lean_string_to_utf8"]
 def String.toUTF8 (a : @& String) : ByteArray :=
-  a.toByteArray
+  a.bytes
 
-@[simp] theorem String.toUTF8_eq_toByteArray {s : String} : s.toUTF8 = s.toByteArray := (rfl)
+@[simp] theorem String.toUTF8_eq_bytes {s : String} : s.toUTF8 = s.bytes := (rfl)
 
-@[simp] theorem String.toByteArray_empty : "".toByteArray = ByteArray.empty := (rfl)
+@[simp] theorem String.bytes_empty : "".bytes = ByteArray.empty := (rfl)
 
 /--
 Appends two strings. Usually accessed via the `++` operator.
@@ -92,33 +92,33 @@ Examples:
 -/
 @[extern "lean_string_append", expose]
 def String.append (s : String) (t : @& String) : String where
-  toByteArray := s.toByteArray ++ t.toByteArray
+  bytes := s.bytes ++ t.bytes
   isValidUTF8 := s.isValidUTF8.append t.isValidUTF8
 
 instance : Append String where
   append s t := s.append t
 
 @[simp]
-theorem String.toByteArray_append {s t : String} : (s ++ t).toByteArray = s.toByteArray ++ t.toByteArray := (rfl)
+theorem String.bytes_append {s t : String} : (s ++ t).bytes = s.bytes ++ t.bytes := (rfl)
 
-theorem String.toByteArray_inj {s t : String} : s.toByteArray = t.toByteArray ↔ s = t := by
+theorem String.bytes_inj {s t : String} : s.bytes = t.bytes ↔ s = t := by
   refine ⟨fun h => ?_, (· ▸ rfl)⟩
   rcases s with ⟨s⟩
   rcases t with ⟨t⟩
   subst h
   rfl
 
-@[simp] theorem String.toByteArray_ofList {l : List Char} : (String.ofList l).toByteArray = l.utf8Encode := by
+@[simp] theorem String.bytes_ofList {l : List Char} : (String.ofList l).bytes = l.utf8Encode := by
   simp [String.ofList]
 
-@[deprecated String.toByteArray_ofList (since := "2025-10-30")]
-theorem List.toByteArray_asString {l : List Char} : (String.ofList l).toByteArray = l.utf8Encode :=
-  String.toByteArray_ofList
+@[deprecated String.bytes_ofList (since := "2025-10-30")]
+theorem List.bytes_asString {l : List Char} : (String.ofList l).bytes = l.utf8Encode :=
+  String.bytes_ofList
 
 theorem String.exists_eq_ofList (s : String) :
     ∃ l : List Char, s = String.ofList l := by
   rcases s with ⟨_, ⟨l, rfl⟩⟩
-  refine ⟨l, by simp [← String.toByteArray_inj]⟩
+  refine ⟨l, by simp [← String.bytes_inj]⟩
 
 @[deprecated String.exists_eq_ofList (since := "2025-10-30")]
 theorem String.exists_eq_asString (s : String) :
@@ -134,14 +134,18 @@ theorem String.utf8ByteSize_append {s t : String} :
   simp [utf8ByteSize]
 
 @[simp]
-theorem String.size_toByteArray {s : String} : s.toByteArray.size = s.utf8ByteSize := rfl
+theorem String.size_bytes {s : String} : s.bytes.size = s.utf8ByteSize := rfl
 
 @[simp]
-theorem String.toByteArray_push {s : String} {c : Char} : (s.push c).toByteArray = s.toByteArray ++ [c].utf8Encode := by
+theorem String.bytes_push {s : String} {c : Char} : (s.push c).bytes = s.bytes ++ [c].utf8Encode := by
   simp [push]
 
 namespace String
 
+@[deprecated rawEndPos (since := "2025-10-20")]
+def endPos (s : String) : String.Pos.Raw :=
+  s.rawEndPos
+
 /-- The start position of the string, as a `String.Pos.Raw.` -/
 def rawStartPos (_s : String) : String.Pos.Raw :=
   0
@@ -160,11 +164,11 @@ theorem utf8ByteSize_ofByteArray {b : ByteArray} {h} :
     (String.ofByteArray b h).utf8ByteSize = b.size := rfl
 
 @[simp]
-theorem toByteArray_singleton {c : Char} : (String.singleton c).toByteArray = [c].utf8Encode := by
+theorem bytes_singleton {c : Char} : (String.singleton c).bytes = [c].utf8Encode := by
   simp [singleton]
 
 theorem singleton_eq_ofList {c : Char} : String.singleton c = String.ofList [c] := by
-  simp [← String.toByteArray_inj]
+  simp [← String.bytes_inj]
 
 @[deprecated singleton_eq_ofList (since := "2025-10-30")]
 theorem singleton_eq_asString {c : Char} : String.singleton c = String.ofList [c] :=
@@ -172,20 +176,20 @@ theorem singleton_eq_asString {c : Char} : String.singleton c = String.ofList [c
 
 @[simp]
 theorem append_singleton {s : String} {c : Char} : s ++ singleton c = s.push c := by
-  simp [← toByteArray_inj]
+  simp [← bytes_inj]
 
 @[simp]
 theorem append_left_inj {s₁ s₂ : String} (t : String) :
     s₁ ++ t = s₂ ++ t ↔ s₁ = s₂ := by
-  simp [← toByteArray_inj]
+  simp [← bytes_inj]
 
 theorem append_assoc {s₁ s₂ s₃ : String} : s₁ ++ s₂ ++ s₃ = s₁ ++ (s₂ ++ s₃) := by
-  simp [← toByteArray_inj, ByteArray.append_assoc]
+  simp [← bytes_inj, ByteArray.append_assoc]
 
 @[simp]
 theorem utf8ByteSize_eq_zero_iff {s : String} : s.utf8ByteSize = 0 ↔ s = "" := by
   refine ⟨fun h => ?_, fun h => h ▸ utf8ByteSize_empty⟩
-  simpa [← toByteArray_inj, ← ByteArray.size_eq_zero_iff] using h
+  simpa [← bytes_inj, ← ByteArray.size_eq_zero_iff] using h
 
 theorem rawEndPos_eq_zero_iff {b : String} : b.rawEndPos = 0 ↔ b = "" := by
   simp
@@ -296,14 +300,14 @@ Examples:
 -/
 structure Pos.Raw.IsValid (s : String) (off : String.Pos.Raw) : Prop where private mk ::
   le_rawEndPos : off ≤ s.rawEndPos
-  isValidUTF8_extract_zero : (s.toByteArray.extract 0 off.byteIdx).IsValidUTF8
+  isValidUTF8_extract_zero : (s.bytes.extract 0 off.byteIdx).IsValidUTF8
 
 theorem Pos.Raw.IsValid.le_utf8ByteSize {s : String} {off : String.Pos.Raw} (h : off.IsValid s) :
     off.byteIdx ≤ s.utf8ByteSize := by
   simpa [Pos.Raw.le_iff] using h.le_rawEndPos
 
 theorem Pos.Raw.isValid_iff_isValidUTF8_extract_zero {s : String} {p : Pos.Raw} :
-    p.IsValid s ↔ p ≤ s.rawEndPos ∧ (s.toByteArray.extract 0 p.byteIdx).IsValidUTF8 :=
+    p.IsValid s ↔ p ≤ s.rawEndPos ∧ (s.bytes.extract 0 p.byteIdx).IsValidUTF8 :=
   ⟨fun ⟨h₁, h₂⟩ => ⟨h₁, h₂⟩, fun ⟨h₁, h₂⟩ => ⟨h₁, h₂⟩⟩
 
 @[deprecated le_rawEndPos (since := "2025-10-20")]
@@ -319,7 +323,7 @@ theorem Pos.Raw.isValid_zero {s : String} : (0 : Pos.Raw).IsValid s where
 @[simp]
 theorem Pos.Raw.isValid_rawEndPos {s : String} : s.rawEndPos.IsValid s where
   le_rawEndPos := by simp
-  isValidUTF8_extract_zero := by simp [← size_toByteArray, s.isValidUTF8]
+  isValidUTF8_extract_zero := by simp [← size_bytes, s.isValidUTF8]
 
 theorem Pos.Raw.isValid_of_eq_rawEndPos {s : String} {p : Pos.Raw} (h : p = s.rawEndPos) :
     p.IsValid s := by
@@ -337,55 +341,55 @@ theorem Pos.Raw.isValid_empty_iff {p : Pos.Raw} : p.IsValid "" ↔ p = 0 := by
     simp
 
 /--
-A `Pos s` is a byte offset in `s` together with a proof that this position is at a UTF-8
+A `ValidPos s` is a byte offset in `s` together with a proof that this position is at a UTF-8
 character boundary.
 -/
 @[ext]
-structure Pos (s : String) where
-  /-- The underlying byte offset of the `Pos`. -/
+structure ValidPos (s : String) where
+  /-- The underlying byte offset of the `ValidPos`. -/
   offset : Pos.Raw
   /-- The proof that `offset` is valid for the string `s`. -/
   isValid : offset.IsValid s
 deriving @[expose] DecidableEq
 
-/-- The start position of `s`, as an `s.Pos`. -/
+/-- The start position of `s`, as an `s.ValidPos`. -/
 @[inline, expose]
-def startPos (s : String) : s.Pos where
+def startValidPos (s : String) : s.ValidPos where
   offset := 0
   isValid := by simp
 
 @[simp]
-theorem offset_startPos {s : String} : s.startPos.offset = 0 := (rfl)
+theorem offset_startValidPos {s : String} : s.startValidPos.offset = 0 := (rfl)
 
-instance {s : String} : Inhabited s.Pos where
-  default := s.startPos
+instance {s : String} : Inhabited s.ValidPos where
+  default := s.startValidPos
 
-/-- The past-the-end position of `s`, as an `s.Pos`. -/
+/-- The past-the-end position of `s`, as an `s.ValidPos`. -/
 @[inline, expose]
-def endPos (s : String) : s.Pos where
+def endValidPos (s : String) : s.ValidPos where
   offset := s.rawEndPos
   isValid := by simp
 
 @[simp]
-theorem offset_endPos {s : String} : s.endPos.offset = s.rawEndPos := (rfl)
+theorem offset_endValidPos {s : String} : s.endValidPos.offset = s.rawEndPos := (rfl)
 
-instance {s : String} : LE s.Pos where
+instance {s : String} : LE s.ValidPos where
   le l r := l.offset ≤ r.offset
 
-instance {s : String} : LT s.Pos where
+instance {s : String} : LT s.ValidPos where
   lt l r := l.offset < r.offset
 
-theorem Pos.le_iff {s : String} {l r : s.Pos} : l ≤ r ↔ l.offset ≤ r.offset :=
+theorem ValidPos.le_iff {s : String} {l r : s.ValidPos} : l ≤ r ↔ l.offset ≤ r.offset :=
   Iff.rfl
 
-theorem Pos.lt_iff {s : String} {l r : s.Pos} : l < r ↔ l.offset < r.offset :=
+theorem ValidPos.lt_iff {s : String} {l r : s.ValidPos} : l < r ↔ l.offset < r.offset :=
   Iff.rfl
 
-instance {s : String} (l r : s.Pos) : Decidable (l ≤ r) :=
-  decidable_of_iff' _ Pos.le_iff
+instance {s : String} (l r : s.ValidPos) : Decidable (l ≤ r) :=
+  decidable_of_iff' _ ValidPos.le_iff
 
-instance {s : String} (l r : s.Pos) : Decidable (l < r) :=
-decidable_of_iff' _ Pos.lt_iff
+instance {s : String} (l r : s.ValidPos) : Decidable (l < r) :=
+decidable_of_iff' _ ValidPos.lt_iff
 
 /--
 A region or slice of some underlying string.
@@ -402,14 +406,14 @@ structure Slice where
   /-- The underlying strings. -/
   str : String
   /-- The byte position of the start of the string slice. -/
-  startInclusive : str.Pos
+  startInclusive : str.ValidPos
   /-- The byte position of the end of the string slice. -/
-  endExclusive : str.Pos
+  endExclusive : str.ValidPos
   /-- The slice is not degenerate (but it may be empty). -/
   startInclusive_le_endExclusive : startInclusive ≤ endExclusive
 
 instance : Inhabited Slice where
-  default := ⟨"", "".startPos, "".startPos, by simp [Pos.le_iff]⟩
+  default := ⟨"", "".startValidPos, "".startValidPos, by simp [ValidPos.le_iff]⟩
 
 /--
 Returns a slice that contains the entire string.
@@ -417,18 +421,15 @@ Returns a slice that contains the entire string.
 @[inline, expose] -- expose for the defeq `s.toSlice.str = s`.
 def toSlice (s : String) : Slice where
   str := s
-  startInclusive := s.startPos
-  endExclusive := s.endPos
-  startInclusive_le_endExclusive := by simp [Pos.le_iff, Pos.Raw.le_iff]
-
-instance : Coe String String.Slice where
-  coe := String.toSlice
+  startInclusive := s.startValidPos
+  endExclusive := s.endValidPos
+  startInclusive_le_endExclusive := by simp [ValidPos.le_iff, Pos.Raw.le_iff]
 
 @[simp]
-theorem startInclusive_toSlice {s : String} : s.toSlice.startInclusive = s.startPos := rfl
+theorem startInclusive_toSlice {s : String} : s.toSlice.startInclusive = s.startValidPos := rfl
 
 @[simp]
-theorem endExclusive_toSlice {s : String} : s.toSlice.endExclusive = s.endPos := rfl
+theorem endExclusive_toSlice {s : String} : s.toSlice.endExclusive = s.endValidPos := rfl
 
 @[simp]
 theorem str_toSlice {s : String} : s.toSlice.str = s := rfl
@@ -531,7 +532,7 @@ instance {s : Slice} : Inhabited s.Pos where
 theorem Slice.offset_startInclusive_add_self {s : Slice} :
     s.startInclusive.offset + s = s.endExclusive.offset := by
   have := s.startInclusive_le_endExclusive
-  simp_all [String.Pos.Raw.ext_iff, Pos.le_iff, Pos.Raw.le_iff, utf8ByteSize_eq]
+  simp_all [String.Pos.Raw.ext_iff, ValidPos.le_iff, Pos.Raw.le_iff, utf8ByteSize_eq]
 
 @[simp]
 theorem Pos.Raw.offsetBy_rawEndPos_left {p : Pos.Raw} {s : String} :
@@ -590,18 +591,18 @@ instance {s : Slice} (l r : s.Pos) : Decidable (l < r) :=
   decidable_of_iff' _ Slice.Pos.lt_iff
 
 /--
-`pos.IsAtEnd` is just shorthand for `pos = s.endPos` that is easier to write if `s` is long.
+`pos.IsAtEnd` is just shorthand for `pos = s.endValidPos` that is easier to write if `s` is long.
 -/
-abbrev Pos.IsAtEnd {s : String} (pos : s.Pos) : Prop :=
-  pos = s.endPos
+abbrev ValidPos.IsAtEnd {s : String} (pos : s.ValidPos) : Prop :=
+  pos = s.endValidPos
 
 @[simp]
-theorem Pos.isAtEnd_iff {s : String} {pos : s.Pos} :
-    pos.IsAtEnd ↔ pos = s.endPos := Iff.rfl
+theorem ValidPos.isAtEnd_iff {s : String} {pos : s.ValidPos} :
+    pos.IsAtEnd ↔ pos = s.endValidPos := Iff.rfl
 
 @[inline]
-instance {s : String} {pos : s.Pos} : Decidable pos.IsAtEnd :=
-  decidable_of_iff _ Pos.isAtEnd_iff
+instance {s : String} {pos : s.ValidPos} : Decidable pos.IsAtEnd :=
+  decidable_of_iff _ ValidPos.isAtEnd_iff
 
 /--
 `pos.IsAtEnd` is just shorthand for `pos = s.endPos` that is easier to write if `s` is long.
@@ -638,20 +639,4 @@ def toSubstring (s : String) : Substring.Raw :=
 def toSubstring' (s : String) : Substring.Raw :=
   s.toRawSubstring'
 
-@[deprecated String.Pos (since := "2025-11-24")]
-abbrev ValidPos (s : String) : Type :=
-  s.Pos
-
-@[deprecated String.startPos (since := "2025-11-24")]
-abbrev startValidPos (s : String) : s.Pos :=
-  s.startPos
-
-@[deprecated String.endPos (since := "2025-11-24")]
-abbrev endValidPos (s : String) : s.Pos :=
-  s.endPos
-
-@[deprecated String.toByteArray (since := "2025-11-24")]
-abbrev String.bytes (s : String) : ByteArray :=
-  s.toByteArray
-
 end String

src/Init/Data/String/Extra.lean

@@ -29,28 +29,28 @@ abbrev validateUTF8 (a : ByteArray) : Bool :=
   a.validateUTF8
 
 private def findLeadingSpacesSize (s : String) : Nat :=
-  let it := s.startPos
-  let it := it.find? (· == '\n') |>.bind String.Pos.next?
+  let it := s.startValidPos
+  let it := it.find? (· == '\n') |>.bind String.ValidPos.next?
   match it with
   | some it => consumeSpaces it 0 s.length
   | none => 0
 where
-  consumeSpaces {s : String} (it : s.Pos) (curr min : Nat) : Nat :=
+  consumeSpaces {s : String} (it : s.ValidPos) (curr min : Nat) : Nat :=
     if h : it.IsAtEnd then min
     else if it.get h == ' ' || it.get h == '\t' then consumeSpaces (it.next h) (curr + 1) min
     else if it.get h == '\n' then findNextLine (it.next h) min
     else findNextLine (it.next h) (Nat.min curr min)
   termination_by it
-  findNextLine {s : String} (it : s.Pos) (min : Nat) : Nat :=
+  findNextLine {s : String} (it : s.ValidPos) (min : Nat) : Nat :=
     if h : it.IsAtEnd then min
     else if it.get h == '\n' then consumeSpaces (it.next h) 0 min
     else findNextLine (it.next h) min
   termination_by it
 
 private def removeNumLeadingSpaces (n : Nat) (s : String) : String :=
-  consumeSpaces n s.startPos ""
+  consumeSpaces n s.startValidPos ""
 where
-  consumeSpaces (n : Nat) {s : String} (it : s.Pos) (r : String) : String :=
+  consumeSpaces (n : Nat) {s : String} (it : s.ValidPos) (r : String) : String :=
      match n with
      | 0 => saveLine it r
      | n+1 =>
@@ -58,7 +58,7 @@ where
        else if it.get h == ' ' || it.get h == '\t' then consumeSpaces n (it.next h) r
        else saveLine it r
   termination_by (it, 1)
-  saveLine {s : String} (it : s.Pos) (r : String) : String :=
+  saveLine {s : String} (it : s.ValidPos) (r : String) : String :=
     if h : it.IsAtEnd then r
     else if it.get h  == '\n' then consumeSpaces n (it.next h) (r.push '\n')
     else saveLine (it.next h) (r.push (it.get h))

src/Init/Data/String/Grind.lean

@@ -1,112 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Author: Markus Himmel
--/
-module
-
-prelude
-public import Init.Data.String.Defs
-public import Init.Grind.ToInt
-
-public section
-
-/-!
-# Register string positions with `grind`.
--/
-
-namespace String
-
-namespace Internal
-
-scoped macro "order" : tactic => `(tactic| {
-    simp [Pos.Raw.lt_iff, Pos.Raw.le_iff, String.Pos.lt_iff, String.Pos.le_iff, Slice.Pos.lt_iff,
-      Slice.Pos.le_iff, Pos.Raw.ext_iff, String.Pos.ext_iff, Slice.Pos.ext_iff] at *;
-    try omega })
-
-end Internal
-
-open Internal
-
-namespace Pos.Raw
-
-instance : Lean.Grind.ToInt String.Pos.Raw (.ci 0) where
-  toInt p := p.byteIdx
-  toInt_inj p q := by simp [Pos.Raw.ext_iff, ← Int.ofNat_inj]
-  toInt_mem := by simp
-
-@[simp]
-theorem toInt_eq {p : Pos.Raw} : Lean.Grind.ToInt.toInt p = p.byteIdx := rfl
-
-instance : Lean.Grind.ToInt.LE String.Pos.Raw (.ci 0) where
-  le_iff := by simp [Pos.Raw.le_iff]
-
-instance : Lean.Grind.ToInt.LT String.Pos.Raw (.ci 0) where
-  lt_iff := by simp [Pos.Raw.lt_iff]
-
-instance : Std.LawfulOrderLT String.Pos.Raw where
-  lt_iff := by order
-
-instance : Std.IsLinearOrder String.Pos.Raw where
-  le_refl := by order
-  le_trans := by order
-  le_antisymm := by order
-  le_total := by order
-
-end Pos.Raw
-
-namespace Pos
-
-instance {s : String} : Lean.Grind.ToInt s.Pos (.co 0 (s.utf8ByteSize + 1)) where
-  toInt p := p.offset.byteIdx
-  toInt_inj p q := by simp [Pos.ext_iff, Pos.Raw.ext_iff, ← Int.ofNat_inj]
-  toInt_mem p := by have := p.isValid.le_utf8ByteSize; simp; omega
-
-@[simp]
-theorem toInt_eq {s : String} {p : s.Pos} : Lean.Grind.ToInt.toInt p = p.offset.byteIdx := rfl
-
-instance {s : String} : Lean.Grind.ToInt.LE s.Pos (.co 0 (s.utf8ByteSize + 1)) where
-  le_iff := by simp [Pos.le_iff, Pos.Raw.le_iff]
-
-instance {s : String} : Lean.Grind.ToInt.LT s.Pos (.co 0 (s.utf8ByteSize + 1)) where
-  lt_iff := by simp [Pos.lt_iff, Pos.Raw.lt_iff]
-
-instance {s : String} : Std.LawfulOrderLT s.Pos where
-  lt_iff := by order
-
-instance {s : String} : Std.IsLinearOrder s.Pos where
-  le_refl := by order
-  le_trans := by order
-  le_antisymm := by order
-  le_total := by order
-
-end Pos
-
-namespace Slice.Pos
-
-instance {s : Slice} : Lean.Grind.ToInt s.Pos (.co 0 (s.utf8ByteSize + 1)) where
-  toInt p := p.offset.byteIdx
-  toInt_inj p q := by simp [Pos.ext_iff, Pos.Raw.ext_iff, ← Int.ofNat_inj]
-  toInt_mem p := by have := p.isValidForSlice.le_utf8ByteSize; simp; omega
-
-@[simp]
-theorem toInt_eq {s : Slice} {p : s.Pos} : Lean.Grind.ToInt.toInt p = p.offset.byteIdx := rfl
-
-instance {s : Slice} : Lean.Grind.ToInt.LE s.Pos (.co 0 (s.utf8ByteSize + 1)) where
-  le_iff := by simp [Pos.le_iff, Pos.Raw.le_iff]
-
-instance {s : Slice} : Lean.Grind.ToInt.LT s.Pos (.co 0 (s.utf8ByteSize + 1)) where
-  lt_iff := by simp [Pos.lt_iff, Pos.Raw.lt_iff]
-
-instance {s : Slice} : Std.LawfulOrderLT s.Pos where
-  lt_iff := by order
-
-instance {s : Slice} : Std.IsLinearOrder s.Pos where
-  le_refl := by order
-  le_trans := by order
-  le_antisymm := by order
-  le_total := by order
-
-end Slice.Pos
-
-end String

src/Init/Data/String/Iterator.lean

@@ -25,9 +25,9 @@ An iterator over the characters (Unicode code points) in a `String`. Typically c
 `String.iter`.
 
 This is a no-longer-supported legacy API that will be removed in a future release. You should use
-`String.Pos` instead, which is similar, but safer. To iterate over a string `s`, start with
-`p : s.startPos`, advance it using `p.next`, access the current character using `p.get` and
-check if the position is at the end using `p = s.endPos` or `p.IsAtEnd`.
+`String.ValidPos` instead, which is similar, but safer. To iterate over a string `s`, start with
+`p : s.startValidPos`, advance it using `p.next`, access the current character using `p.get` and
+check if the position is at the end using `p = s.endValidPos` or `p.IsAtEnd`.
 
 String iterators pair a string with a valid byte index. This allows efficient character-by-character
 processing of strings while avoiding the need to manually ensure that byte indices are used with the
@@ -57,9 +57,9 @@ structure Iterator where
 /-- Creates an iterator at the beginning of the string.
 
 This is a no-longer-supported legacy API that will be removed in a future release. You should use
-`String.Pos` instead, which is similar, but safer. To iterate over a string `s`, start with
-`p : s.startPos`, advance it using `p.next`, access the current character using `p.get` and
-check if the position is at the end using `p = s.endPos` or `p.IsAtEnd`.
+`String.ValidPos` instead, which is similar, but safer. To iterate over a string `s`, start with
+`p : s.startValidPos`, advance it using `p.next`, access the current character using `p.get` and
+check if the position is at the end using `p = s.endValidPos` or `p.IsAtEnd`.
 -/
 @[inline] def mkIterator (s : String) : Iterator :=
   ⟨s, 0⟩
@@ -95,9 +95,9 @@ def pos := Iterator.i
 Gets the character at the iterator's current position.
 
 This is a no-longer-supported legacy API that will be removed in a future release. You should use
-`String.Pos` instead, which is similar, but safer. To iterate over a string `s`, start with
-`p : s.startPos`, advance it using `p.next`, access the current character using `p.get` and
-check if the position is at the end using `p = s.endPos` or `p.IsAtEnd`.
+`String.ValidPos` instead, which is similar, but safer. To iterate over a string `s`, start with
+`p : s.startValidPos`, advance it using `p.next`, access the current character using `p.get` and
+check if the position is at the end using `p = s.endValidPos` or `p.IsAtEnd`.
 
 A run-time bounds check is performed. Use `String.Iterator.curr'` to avoid redundant bounds checks.
 
@@ -110,9 +110,9 @@ If the position is invalid, returns `(default : Char)`.
 Moves the iterator's position forward by one character, unconditionally.
 
 This is a no-longer-supported legacy API that will be removed in a future release. You should use
-`String.Pos` instead, which is similar, but safer. To iterate over a string `s`, start with
-`p : s.startPos`, advance it using `p.next`, access the current character using `p.get` and
-check if the position is at the end using `p = s.endPos` or `p.IsAtEnd`.
+`String.ValidPos` instead, which is similar, but safer. To iterate over a string `s`, start with
+`p : s.startValidPos`, advance it using `p.next`, access the current character using `p.get` and
+check if the position is at the end using `p = s.endValidPos` or `p.IsAtEnd`.
 
 It is only valid to call this function if the iterator is not at the end of the string (i.e.
 if `Iterator.atEnd` is `false`); otherwise, the resulting iterator will be invalid.

src/Init/Data/String/Lemmas.lean

@@ -8,7 +8,6 @@ module
 prelude
 public import Init.Data.String.Lemmas.Splits
 public import Init.Data.String.Lemmas.Modify
-public import Init.Data.String.Lemmas.Search
 public import Init.Data.Char.Order
 public import Init.Data.Char.Lemmas
 public import Init.Data.List.Lex

src/Init/Data/String/Lemmas/Basic.lean

@@ -41,11 +41,11 @@ theorem singleton_ne_empty {c : Char} : singleton c ≠ "" := by
 
 @[simp]
 theorem Slice.Pos.toCopy_inj {s : Slice} {p₁ p₂ : s.Pos} : p₁.toCopy = p₂.toCopy ↔ p₁ = p₂ := by
-  simp [String.Pos.ext_iff, Pos.ext_iff]
+  simp [Pos.ext_iff, ValidPos.ext_iff]
 
 @[simp]
-theorem Pos.startPos_le {s : String} (p : s.Pos) : s.startPos ≤ p := by
-  simp [Pos.le_iff, Pos.Raw.le_iff]
+theorem ValidPos.startValidPos_le {s : String} (p : s.ValidPos) : s.startValidPos ≤ p := by
+  simp [ValidPos.le_iff, Pos.Raw.le_iff]
 
 @[simp]
 theorem Slice.Pos.startPos_le {s : Slice} (p : s.Pos) : s.startPos ≤ p := by

src/Init/Data/String/Lemmas/Modify.lean

@@ -22,22 +22,22 @@ public section
 
 namespace String
 
-/-- You might want to invoke `Pos.Splits.exists_eq_singleton_append` to be able to apply this. -/
-theorem Pos.Splits.pastSet {s : String} {p : s.Pos} {t₁ t₂ : String}
+/-- You might want to invoke `ValidPos.Splits.exists_eq_singleton_append` to be able to apply this. -/
+theorem ValidPos.Splits.pastSet {s : String} {p : s.ValidPos} {t₁ t₂ : String}
     {c d : Char} (h : p.Splits t₁ (singleton c ++ t₂)) :
-    (p.pastSet d h.ne_endPos_of_singleton).Splits (t₁ ++ singleton d) t₂ := by
-  generalize h.ne_endPos_of_singleton = hp
+    (p.pastSet d h.ne_endValidPos_of_singleton).Splits (t₁ ++ singleton d) t₂ := by
+  generalize h.ne_endValidPos_of_singleton = hp
   obtain ⟨rfl, rfl, rfl⟩ := by simpa using h.eq (p.splits_next_right hp)
   apply splits_pastSet
 
-/-- You might want to invoke `Pos.Splits.exists_eq_singleton_append` to be able to apply this. -/
-theorem Pos.Splits.pastModify {s : String} {p : s.Pos} {t₁ t₂ : String}
+/-- You might want to invoke `ValidPos.Splits.exists_eq_singleton_append` to be able to apply this. -/
+theorem ValidPos.Splits.pastModify {s : String} {p : s.ValidPos} {t₁ t₂ : String}
     {c : Char} (h : p.Splits t₁ (singleton c ++ t₂)) :
-    (p.pastModify f h.ne_endPos_of_singleton).Splits
-    (t₁ ++ singleton (f (p.get h.ne_endPos_of_singleton))) t₂ :=
+    (p.pastModify f h.ne_endValidPos_of_singleton).Splits
+    (t₁ ++ singleton (f (p.get h.ne_endValidPos_of_singleton))) t₂ :=
   h.pastSet
 
-theorem toList_mapAux {f : Char → Char} {s : String} {p : s.Pos}
+theorem toList_mapAux {f : Char → Char} {s : String} {p : s.ValidPos}
     (h : p.Splits t₁ t₂) : (mapAux f s p).toList = t₁.toList ++ t₂.toList.map f := by
   fun_induction mapAux generalizing t₁ t₂ with
   | case1 s => simp_all
@@ -47,7 +47,7 @@ theorem toList_mapAux {f : Char → Char} {s : String} {p : s.Pos}
 
 @[simp]
 theorem toList_map {f : Char → Char} {s : String} : (s.map f).toList = s.toList.map f := by
-  simp [map, toList_mapAux s.splits_startPos]
+  simp [map, toList_mapAux s.splits_startValidPos]
 
 @[simp]
 theorem length_map {f : Char → Char} {s : String} : (s.map f).length = s.length := by

src/Init/Data/String/Lemmas/Search.lean

@@ -1,32 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel
--/
-module
-
-prelude
-public import Init.Data.String.Search
-import all Init.Data.String.Search
-
-public section
-
-namespace String
-open String.Slice Pattern
-
-variable {ρ : Type} {σ : Slice → Type}
-variable [∀ s, Std.Iterators.Iterator (σ s) Id (SearchStep s)]
-variable [∀ s, Std.Iterators.Finite (σ s) Id]
-variable [∀ s, Std.Iterators.IteratorLoop (σ s) Id Id]
-
-@[simp]
-theorem Slice.Pos.le_find {s : Slice} (pos : s.Pos) (pattern : ρ) [ToForwardSearcher pattern σ] :
-    pos ≤ pos.find pattern := by
-  simp [Slice.Pos.find]
-
-@[simp]
-theorem Pos.le_find {s : String} (pos : s.Pos) (pattern : ρ) [ToForwardSearcher pattern σ] :
-    pos ≤ pos.find pattern := by
-  simp [Pos.find, ← toSlice_le]
-
-end String

src/Init/Data/String/Lemmas/Splits.lean

@@ -11,7 +11,7 @@ import Init.Data.ByteArray.Lemmas
 import Init.Data.String.Lemmas.Basic
 
 /-!
-# `Splits` predicates on `String.Pos` and `String.Slice.Pos`.
+# `Splits` predicates on `String.ValidPos` and `String.Slice.Pos`.
 
 We introduce the predicate `p.Splits t₁ t₂` for a position `p` on a string or slice `s`, which means
 that `s = t₁ ++ t₂` with `p` lying between the two parts. This is a useful primitive when verifying
@@ -26,7 +26,7 @@ namespace String
 We say that `p` splits `s` into `t₁` and `t₂` if `s = t₁ ++ t₂` and `p` is the position between `t₁`
 and `t₂`.
 -/
-structure Pos.Splits {s : String} (p : s.Pos) (t₁ t₂ : String) : Prop where
+structure ValidPos.Splits {s : String} (p : s.ValidPos) (t₁ t₂ : String) : Prop where
   eq_append : s = t₁ ++ t₂
   offset_eq_rawEndPos : p.offset = t₁.rawEndPos
 
@@ -39,11 +39,11 @@ structure Slice.Pos.Splits {s : Slice} (p : s.Pos) (t₁ t₂ : String) : Prop w
   offset_eq_rawEndPos : p.offset = t₁.rawEndPos
 
 @[simp]
-theorem Pos.splits_cast_iff {s₁ s₂ : String} {h : s₁ = s₂} {p : s₁.Pos} {t₁ t₂ : String} :
+theorem ValidPos.splits_cast_iff {s₁ s₂ : String} {h : s₁ = s₂} {p : s₁.ValidPos} {t₁ t₂ : String} :
     (p.cast h).Splits t₁ t₂ ↔ p.Splits t₁ t₂ := by
   subst h; simp
 
-theorem Pos.Splits.cast {s₁ s₂ : String} {p : s₁.Pos} {t₁ t₂ : String} (h : s₁ = s₂) :
+theorem ValidPos.Splits.cast {s₁ s₂ : String} {p : s₁.ValidPos} {t₁ t₂ : String} (h : s₁ = s₂) :
     p.Splits t₁ t₂ → (p.cast h).Splits t₁ t₂ :=
   splits_cast_iff.mpr
 
@@ -72,17 +72,17 @@ theorem Slice.Pos.splits_toCopy_iff {s : Slice} {p : s.Pos} {t₁ t₂ : String}
   ⟨splits_of_splits_toCopy, (·.toCopy)⟩
 
 @[simp]
-theorem Pos.splits_toSlice_iff {s : String} {p : s.Pos} {t₁ t₂ : String} :
+theorem ValidPos.splits_toSlice_iff {s : String} {p : s.ValidPos} {t₁ t₂ : String} :
     p.toSlice.Splits t₁ t₂ ↔ p.Splits t₁ t₂ := by
   rw [← Slice.Pos.splits_toCopy_iff, p.toCopy_toSlice_eq_cast, splits_cast_iff]
 
-theorem Pos.Splits.toSlice {s : String} {p : s.Pos} {t₁ t₂ : String}
+theorem ValidPos.Splits.toSlice {s : String} {p : s.ValidPos} {t₁ t₂ : String}
     (h : p.Splits t₁ t₂) : p.toSlice.Splits t₁ t₂ :=
   splits_toSlice_iff.mpr h
 
-theorem Pos.splits {s : String} (p : s.Pos) :
+theorem ValidPos.splits {s : String} (p : s.ValidPos) :
     p.Splits (s.sliceTo p).copy (s.sliceFrom p).copy where
-  eq_append := by simp [← toByteArray_inj, Slice.toByteArray_copy, ← size_toByteArray]
+  eq_append := by simp [← bytes_inj, Slice.bytes_copy, ← size_bytes]
   offset_eq_rawEndPos := by simp
 
 theorem Slice.Pos.splits {s : Slice} (p : s.Pos) :
@@ -90,23 +90,23 @@ theorem Slice.Pos.splits {s : Slice} (p : s.Pos) :
   eq_append := copy_eq_copy_sliceTo
   offset_eq_rawEndPos := by simp
 
-theorem Pos.Splits.toByteArray_left_eq {s : String} {p : s.Pos} {t₁ t₂}
-    (h : p.Splits t₁ t₂) : t₁.toByteArray = s.toByteArray.extract 0 p.offset.byteIdx := by
+theorem ValidPos.Splits.bytes_left_eq {s : String} {p : s.ValidPos} {t₁ t₂}
+    (h : p.Splits t₁ t₂) : t₁.bytes = s.bytes.extract 0 p.offset.byteIdx := by
   simp [h.eq_append, h.offset_eq_rawEndPos, ByteArray.extract_append_eq_left]
 
-theorem Pos.Splits.toByteArray_right_eq {s : String} {p : s.Pos} {t₁ t₂}
-    (h : p.Splits t₁ t₂) : t₂.toByteArray = s.toByteArray.extract p.offset.byteIdx s.utf8ByteSize := by
+theorem ValidPos.Splits.bytes_right_eq {s : String} {p : s.ValidPos} {t₁ t₂}
+    (h : p.Splits t₁ t₂) : t₂.bytes = s.bytes.extract p.offset.byteIdx s.utf8ByteSize := by
   simp [h.eq_append, h.offset_eq_rawEndPos, ByteArray.extract_append_eq_right]
 
-theorem Pos.Splits.eq_left {s : String} {p : s.Pos} {t₁ t₂ t₃ t₄}
+theorem ValidPos.Splits.eq_left {s : String} {p : s.ValidPos} {t₁ t₂ t₃ t₄}
     (h₁ : p.Splits t₁ t₂) (h₂ : p.Splits t₃ t₄) : t₁ = t₃ := by
-  rw [← String.toByteArray_inj, h₁.toByteArray_left_eq, h₂.toByteArray_left_eq]
+  rw [← String.bytes_inj, h₁.bytes_left_eq, h₂.bytes_left_eq]
 
-theorem Pos.Splits.eq_right {s : String} {p : s.Pos} {t₁ t₂ t₃ t₄}
+theorem ValidPos.Splits.eq_right {s : String} {p : s.ValidPos} {t₁ t₂ t₃ t₄}
     (h₁ : p.Splits t₁ t₂) (h₂ : p.Splits t₃ t₄) : t₂ = t₄ := by
-  rw [← String.toByteArray_inj, h₁.toByteArray_right_eq, h₂.toByteArray_right_eq]
+  rw [← String.bytes_inj, h₁.bytes_right_eq, h₂.bytes_right_eq]
 
-theorem Pos.Splits.eq {s : String} {p : s.Pos} {t₁ t₂ t₃ t₄}
+theorem ValidPos.Splits.eq {s : String} {p : s.ValidPos} {t₁ t₂ t₃ t₄}
     (h₁ : p.Splits t₁ t₂) (h₂ : p.Splits t₃ t₄) : t₁ = t₃ ∧ t₂ = t₄ :=
   ⟨h₁.eq_left h₂, h₁.eq_right h₂⟩
 
@@ -123,35 +123,35 @@ theorem Slice.Pos.Splits.eq {s : Slice} {p : s.Pos} {t₁ t₂ t₃ t₄}
   (splits_toCopy_iff.2 h₁).eq (splits_toCopy_iff.2 h₂)
 
 @[simp]
-theorem splits_endPos (s : String) : s.endPos.Splits s "" where
+theorem splits_endValidPos (s : String) : s.endValidPos.Splits s "" where
   eq_append := by simp
   offset_eq_rawEndPos := by simp
 
 @[simp]
-theorem splits_endPos_iff {s : String} :
-    s.endPos.Splits t₁ t₂ ↔ t₁ = s ∧ t₂ = "" :=
-  ⟨fun h => ⟨h.eq_left s.splits_endPos, h.eq_right s.splits_endPos⟩,
-   by rintro ⟨rfl, rfl⟩; exact t₁.splits_endPos⟩
+theorem splits_endValidPos_iff {s : String} :
+    s.endValidPos.Splits t₁ t₂ ↔ t₁ = s ∧ t₂ = "" :=
+  ⟨fun h => ⟨h.eq_left s.splits_endValidPos, h.eq_right s.splits_endValidPos⟩,
+   by rintro ⟨rfl, rfl⟩; exact t₁.splits_endValidPos⟩
 
-theorem Pos.Splits.eq_endPos_iff {s : String} {p : s.Pos} (h : p.Splits t₁ t₂) :
-    p = s.endPos ↔ t₂ = "" :=
-  ⟨fun h' => h.eq_right (h' ▸ s.splits_endPos),
-   by rintro rfl; simp [Pos.ext_iff, h.offset_eq_rawEndPos, h.eq_append]⟩
+theorem ValidPos.Splits.eq_endValidPos_iff {s : String} {p : s.ValidPos} (h : p.Splits t₁ t₂) :
+    p = s.endValidPos ↔ t₂ = "" :=
+  ⟨fun h' => h.eq_right (h' ▸ s.splits_endValidPos),
+   by rintro rfl; simp [ValidPos.ext_iff, h.offset_eq_rawEndPos, h.eq_append]⟩
 
-theorem splits_startPos (s : String) : s.startPos.Splits "" s where
+theorem splits_startValidPos (s : String) : s.startValidPos.Splits "" s where
   eq_append := by simp
   offset_eq_rawEndPos := by simp
 
 @[simp]
-theorem splits_startPos_iff {s : String} :
-    s.startPos.Splits t₁ t₂ ↔ t₁ = "" ∧ t₂ = s :=
-  ⟨fun h => ⟨h.eq_left s.splits_startPos, h.eq_right s.splits_startPos⟩,
-   by rintro ⟨rfl, rfl⟩; exact t₂.splits_startPos⟩
+theorem splits_startValidPos_iff {s : String} :
+    s.startValidPos.Splits t₁ t₂ ↔ t₁ = "" ∧ t₂ = s :=
+  ⟨fun h => ⟨h.eq_left s.splits_startValidPos, h.eq_right s.splits_startValidPos⟩,
+   by rintro ⟨rfl, rfl⟩; exact t₂.splits_startValidPos⟩
 
-theorem Pos.Splits.eq_startPos_iff {s : String} {p : s.Pos} (h : p.Splits t₁ t₂) :
-    p = s.startPos ↔ t₁ = "" :=
-  ⟨fun h' => h.eq_left (h' ▸ s.splits_startPos),
-   by rintro rfl; simp [Pos.ext_iff, h.offset_eq_rawEndPos]⟩
+theorem ValidPos.Splits.eq_startValidPos_iff {s : String} {p : s.ValidPos} (h : p.Splits t₁ t₂) :
+    p = s.startValidPos ↔ t₁ = "" :=
+  ⟨fun h' => h.eq_left (h' ▸ s.splits_startValidPos),
+   by rintro rfl; simp [ValidPos.ext_iff, h.offset_eq_rawEndPos]⟩
 
 @[simp]
 theorem Slice.splits_endPos (s : Slice) : s.endPos.Splits s.copy "" where
@@ -161,11 +161,11 @@ theorem Slice.splits_endPos (s : Slice) : s.endPos.Splits s.copy "" where
 @[simp]
 theorem Slice.splits_endPos_iff {s : Slice} :
     s.endPos.Splits t₁ t₂ ↔ t₁ = s.copy ∧ t₂ = "" := by
-  rw [← Pos.splits_toCopy_iff, ← endPos_copy, String.splits_endPos_iff]
+  rw [← Pos.splits_toCopy_iff, ← endValidPos_copy, splits_endValidPos_iff]
 
 theorem Slice.Pos.Splits.eq_endPos_iff {s : Slice} {p : s.Pos} (h : p.Splits t₁ t₂) :
     p = s.endPos ↔ t₂ = "" := by
-  rw [← toCopy_inj, ← endPos_copy, h.toCopy.eq_endPos_iff]
+  rw [← toCopy_inj, ← endValidPos_copy, h.toCopy.eq_endValidPos_iff]
 
 @[simp]
 theorem Slice.splits_startPos (s : Slice) : s.startPos.Splits "" s.copy where
@@ -175,18 +175,18 @@ theorem Slice.splits_startPos (s : Slice) : s.startPos.Splits "" s.copy where
 @[simp]
 theorem Slice.splits_startPos_iff {s : Slice} :
     s.startPos.Splits t₁ t₂ ↔ t₁ = "" ∧ t₂ = s.copy := by
-  rw [← Pos.splits_toCopy_iff, ← startPos_copy, String.splits_startPos_iff]
+  rw [← Pos.splits_toCopy_iff, ← startValidPos_copy, splits_startValidPos_iff]
 
 theorem Slice.Pos.Splits.eq_startPos_iff {s : Slice} {p : s.Pos} (h : p.Splits t₁ t₂) :
     p = s.startPos ↔ t₁ = "" := by
-  rw [← toCopy_inj, ← startPos_copy, h.toCopy.eq_startPos_iff]
+  rw [← toCopy_inj, ← startValidPos_copy, h.toCopy.eq_startValidPos_iff]
 
-theorem Pos.splits_next_right {s : String} (p : s.Pos) (hp : p ≠ s.endPos) :
+theorem ValidPos.splits_next_right {s : String} (p : s.ValidPos) (hp : p ≠ s.endValidPos) :
     p.Splits (s.sliceTo p).copy (singleton (p.get hp) ++ (s.sliceFrom (p.next hp)).copy) where
   eq_append := by simpa [← append_assoc] using p.eq_copy_sliceTo_append_get hp
   offset_eq_rawEndPos := by simp
 
-theorem Pos.splits_next {s : String} (p : s.Pos) (hp : p ≠ s.endPos) :
+theorem ValidPos.splits_next {s : String} (p : s.ValidPos) (hp : p ≠ s.endValidPos) :
     (p.next hp).Splits ((s.sliceTo p).copy ++ singleton (p.get hp)) (s.sliceFrom (p.next hp)).copy where
   eq_append := p.eq_copy_sliceTo_append_get hp
   offset_eq_rawEndPos := by simp
@@ -201,12 +201,12 @@ theorem Slice.Pos.splits_next {s : Slice} (p : s.Pos) (hp : p ≠ s.endPos) :
   eq_append := p.copy_eq_copy_sliceTo_append_get hp
   offset_eq_rawEndPos := by simp
 
-theorem Pos.Splits.exists_eq_singleton_append {s : String} {p : s.Pos}
-    (hp : p ≠ s.endPos) (h : p.Splits t₁ t₂) : ∃ t₂', t₂ = singleton (p.get hp) ++ t₂' :=
+theorem ValidPos.Splits.exists_eq_singleton_append {s : String} {p : s.ValidPos}
+    (hp : p ≠ s.endValidPos) (h : p.Splits t₁ t₂) : ∃ t₂', t₂ = singleton (p.get hp) ++ t₂' :=
   ⟨(s.sliceFrom (p.next hp)).copy, h.eq_right (p.splits_next_right hp)⟩
 
-theorem Pos.Splits.exists_eq_append_singleton {s : String} {p : s.Pos}
-    (hp : p ≠ s.endPos) (h : (p.next hp).Splits t₁ t₂) : ∃ t₁', t₁ = t₁' ++ singleton (p.get hp) :=
+theorem ValidPos.Splits.exists_eq_append_singleton {s : String} {p : s.ValidPos}
+    (hp : p ≠ s.endValidPos) (h : (p.next hp).Splits t₁ t₂) : ∃ t₁', t₁ = t₁' ++ singleton (p.get hp) :=
   ⟨(s.sliceTo p).copy, h.eq_left (p.splits_next hp)⟩
 
 theorem Slice.Pos.Splits.exists_eq_singleton_append {s : Slice} {p : s.Pos}
@@ -217,13 +217,13 @@ theorem Slice.Pos.Splits.exists_eq_append_singleton {s : Slice} {p : s.Pos}
     (hp : p ≠ s.endPos) (h : (p.next hp).Splits t₁ t₂) : ∃ t₁', t₁ = t₁' ++ singleton (p.get hp) :=
   ⟨(s.sliceTo p).copy, h.eq_left (p.splits_next hp)⟩
 
-theorem Pos.Splits.ne_endPos_of_singleton {s : String} {p : s.Pos}
-    (h : p.Splits t₁ (singleton c ++ t₂)) : p ≠ s.endPos := by
-  simp [h.eq_endPos_iff]
+theorem ValidPos.Splits.ne_endValidPos_of_singleton {s : String} {p : s.ValidPos}
+    (h : p.Splits t₁ (singleton c ++ t₂)) : p ≠ s.endValidPos := by
+  simp [h.eq_endValidPos_iff]
 
-theorem Pos.Splits.ne_startPos_of_singleton {s : String} {p : s.Pos}
-    (h : p.Splits (t₁ ++ singleton c) t₂) : p ≠ s.startPos := by
-  simp [h.eq_startPos_iff]
+theorem ValidPos.Splits.ne_startValidPos_of_singleton {s : String} {p : s.ValidPos}
+    (h : p.Splits (t₁ ++ singleton c) t₂) : p ≠ s.startValidPos := by
+  simp [h.eq_startValidPos_iff]
 
 theorem Slice.Pos.Splits.ne_endPos_of_singleton {s : Slice} {p : s.Pos}
     (h : p.Splits t₁ (singleton c ++ t₂)) : p ≠ s.endPos := by
@@ -233,10 +233,10 @@ theorem Slice.Pos.Splits.ne_startPos_of_singleton {s : Slice} {p : s.Pos}
     (h : p.Splits (t₁ ++ singleton c) t₂) : p ≠ s.startPos := by
   simp [h.eq_startPos_iff]
 
-/-- You might want to invoke `Pos.Splits.exists_eq_singleton_append` to be able to apply this. -/
-theorem Pos.Splits.next {s : String} {p : s.Pos}
-    (h : p.Splits t₁ (singleton c ++ t₂)) : (p.next h.ne_endPos_of_singleton).Splits (t₁ ++ singleton c) t₂ := by
-  generalize h.ne_endPos_of_singleton = hp
+/-- You might want to invoke `ValidPos.Splits.exists_eq_singleton_append` to be able to apply this. -/
+theorem ValidPos.Splits.next {s : String} {p : s.ValidPos}
+    (h : p.Splits t₁ (singleton c ++ t₂)) : (p.next h.ne_endValidPos_of_singleton).Splits (t₁ ++ singleton c) t₂ := by
+  generalize h.ne_endValidPos_of_singleton = hp
   obtain ⟨rfl, rfl, rfl⟩ := by simpa using h.eq (splits_next_right p hp)
   exact splits_next p hp
 

src/Init/Data/String/Modify.lean

@@ -33,28 +33,28 @@ Examples:
 * `("L∃∀N".pos ⟨4⟩ (by decide)).set 'X' (by decide) = "L∃XN"`
 -/
 @[extern "lean_string_utf8_set", expose]
-def Pos.set {s : String} (p : s.Pos) (c : Char) (hp : p ≠ s.endPos) : String :=
+def ValidPos.set {s : String} (p : s.ValidPos) (c : Char) (hp : p ≠ s.endValidPos) : String :=
   if hc : c.utf8Size = 1 ∧ (p.byte hp).utf8ByteSize isUTF8FirstByte_byte = 1 then
-    .ofByteArray (s.toByteArray.set p.offset.byteIdx c.toUInt8 (p.byteIdx_lt_utf8ByteSize hp)) (by
+    .ofByteArray (s.bytes.set p.offset.byteIdx c.toUInt8 (p.byteIdx_lt_utf8ByteSize hp)) (by
       rw [ByteArray.set_eq_push_extract_append_extract, ← hc.2, utf8ByteSize_byte,
-        ← Pos.byteIdx_offset_next]
+        ← ValidPos.byteIdx_offset_next]
       refine ByteArray.IsValidUTF8.append ?_ (p.next hp).isValid.isValidUTF8_extract_utf8ByteSize
       exact p.isValid.isValidUTF8_extract_zero.push hc.1)
   else
     (s.sliceTo p).copy ++ singleton c ++ (s.sliceFrom (p.next hp)).copy
 
-theorem Pos.set_eq_append {s : String} {p : s.Pos} {c : Char} {hp} :
+theorem ValidPos.set_eq_append {s : String} {p : s.ValidPos} {c : Char} {hp} :
     p.set c hp = (s.sliceTo p).copy ++ singleton c ++ (s.sliceFrom (p.next hp)).copy := by
   rw [set]
   split
   · rename_i h
-    simp [← toByteArray_inj, ByteArray.set_eq_push_extract_append_extract, Slice.toByteArray_copy,
+    simp [← bytes_inj, ByteArray.set_eq_push_extract_append_extract, Slice.bytes_copy,
       List.utf8Encode_singleton, String.utf8EncodeChar_eq_singleton h.1, utf8ByteSize_byte ▸ h.2]
   · rfl
 
-theorem Pos.Raw.IsValid.set_of_le {s : String} {p : s.Pos} {c : Char} {hp : p ≠ s.endPos}
+theorem Pos.Raw.IsValid.set_of_le {s : String} {p : s.ValidPos} {c : Char} {hp : p ≠ s.endValidPos}
     {q : Pos.Raw} (hq : q.IsValid s) (hpq : q ≤ p.offset) : q.IsValid (p.set c hp) := by
-  rw [Pos.set_eq_append, String.append_assoc]
+  rw [ValidPos.set_eq_append, String.append_assoc]
   apply append_right
   rw [isValid_copy_iff, isValidForSlice_stringSliceTo]
   exact ⟨hpq, hq⟩
@@ -62,40 +62,40 @@ theorem Pos.Raw.IsValid.set_of_le {s : String} {p : s.Pos} {c : Char} {hp : p
 /-- Given a valid position in a string, obtain the corresponding position after setting a character on
 that string, provided that the position was before the changed position. -/
 @[inline]
-def Pos.toSetOfLE {s : String} (q p : s.Pos) (c : Char) (hp : p ≠ s.endPos)
-    (hpq : q ≤ p) : (p.set c hp).Pos where
+def ValidPos.toSetOfLE {s : String} (q p : s.ValidPos) (c : Char) (hp : p ≠ s.endValidPos)
+    (hpq : q ≤ p) : (p.set c hp).ValidPos where
   offset := q.offset
   isValid := q.isValid.set_of_le hpq
 
 @[simp]
-theorem Pos.offset_toSetOfLE {s : String} {q p : s.Pos} {c : Char} {hp : p ≠ s.endPos}
+theorem ValidPos.offset_toSetOfLE {s : String} {q p : s.ValidPos} {c : Char} {hp : p ≠ s.endValidPos}
     {hpq : q ≤ p} : (q.toSetOfLE p c hp hpq).offset = q.offset := (rfl)
 
-theorem Pos.Raw.isValid_add_char_set {s : String} {p : s.Pos} {c : Char} {hp} :
+theorem Pos.Raw.isValid_add_char_set {s : String} {p : s.ValidPos} {c : Char} {hp} :
     (p.offset + c).IsValid (p.set c hp) :=
-  Pos.set_eq_append ▸ IsValid.append_right (isValid_of_eq_rawEndPos (by simp)) _
+  ValidPos.set_eq_append ▸ IsValid.append_right (isValid_of_eq_rawEndPos (by simp)) _
 
-/-- The position just after the position that changed in a `Pos.set` call. -/
+/-- The position just after the position that changed in a `ValidPos.set` call. -/
 @[inline]
-def Pos.pastSet {s : String} (p : s.Pos) (c : Char) (hp) : (p.set c hp).Pos where
+def ValidPos.pastSet {s : String} (p : s.ValidPos) (c : Char) (hp) : (p.set c hp).ValidPos where
   offset := p.offset + c
   isValid := Pos.Raw.isValid_add_char_set
 
 @[simp]
-theorem Pos.offset_pastSet {s : String} {p : s.Pos} {c : Char} {hp} :
+theorem ValidPos.offset_pastSet {s : String} {p : s.ValidPos} {c : Char} {hp} :
     (p.pastSet c hp).offset = p.offset + c := (rfl)
 
 @[inline]
-def Pos.appendRight {s : String} (p : s.Pos) (t : String) : (s ++ t).Pos where
+def ValidPos.appendRight {s : String} (p : s.ValidPos) (t : String) : (s ++ t).ValidPos where
   offset := p.offset
   isValid := p.isValid.append_right t
 
-theorem Pos.splits_pastSet {s : String} {p : s.Pos} {c : Char} {hp} :
+theorem ValidPos.splits_pastSet {s : String} {p : s.ValidPos} {c : Char} {hp} :
     (p.pastSet c hp).Splits ((s.sliceTo p).copy ++ singleton c) (s.sliceFrom (p.next hp)).copy where
   eq_append := set_eq_append
   offset_eq_rawEndPos := by simp
 
-theorem remainingBytes_pastSet {s : String} {p : s.Pos} {c : Char} {hp} :
+theorem remainingBytes_pastSet {s : String} {p : s.ValidPos} {c : Char} {hp} :
     (p.pastSet c hp).remainingBytes = (p.next hp).remainingBytes := by
   rw [(p.next hp).splits.remainingBytes_eq, p.splits_pastSet.remainingBytes_eq]
 
@@ -110,34 +110,34 @@ Examples:
 * `("abc".pos ⟨1⟩ (by decide)).modify Char.toUpper (by decide) = "aBc"`
 -/
 @[inline]
-def Pos.modify {s : String} (p : s.Pos) (f : Char → Char) (hp : p ≠ s.endPos) :
+def ValidPos.modify {s : String} (p : s.ValidPos) (f : Char → Char) (hp : p ≠ s.endValidPos) :
     String :=
   p.set (f <| p.get hp) hp
 
-theorem Pos.Raw.IsValid.modify_of_le {s : String} {p : s.Pos} {f : Char → Char}
-    {hp : p ≠ s.endPos} {q : Pos.Raw} (hq : q.IsValid s) (hpq : q ≤ p.offset) :
+theorem Pos.Raw.IsValid.modify_of_le {s : String} {p : s.ValidPos} {f : Char → Char}
+    {hp : p ≠ s.endValidPos} {q : Pos.Raw} (hq : q.IsValid s) (hpq : q ≤ p.offset) :
     q.IsValid (p.modify f hp) :=
   set_of_le hq hpq
 
 /-- Given a valid position in a string, obtain the corresponding position after modifying a character
 in that string, provided that the position was before the changed position. -/
 @[inline]
-def Pos.toModifyOfLE {s : String} (q p : s.Pos) (f : Char → Char)
-    (hp : p ≠ s.endPos) (hpq : q ≤ p) : (p.modify f hp).Pos where
+def ValidPos.toModifyOfLE {s : String} (q p : s.ValidPos) (f : Char → Char)
+    (hp : p ≠ s.endValidPos) (hpq : q ≤ p) : (p.modify f hp).ValidPos where
   offset := q.offset
   isValid := q.isValid.modify_of_le hpq
 
 @[simp]
-theorem Pos.offset_toModifyOfLE {s : String} {q p : s.Pos} {f : Char → Char}
-    {hp : p ≠ s.endPos} {hpq : q ≤ p} : (q.toModifyOfLE p f hp hpq).offset = q.offset := (rfl)
+theorem ValidPos.offset_toModifyOfLE {s : String} {q p : s.ValidPos} {f : Char → Char}
+    {hp : p ≠ s.endValidPos} {hpq : q ≤ p} : (q.toModifyOfLE p f hp hpq).offset = q.offset := (rfl)
 
-/-- The position just after the position that was modified in a `Pos.modify` call. -/
+/-- The position just after the position that was modified in a `ValidPos.modify` call. -/
 @[inline]
-def Pos.pastModify {s : String} (p : s.Pos) (f : Char → Char)
-    (hp : p ≠ s.endPos) : (p.modify f hp).Pos :=
+def ValidPos.pastModify {s : String} (p : s.ValidPos) (f : Char → Char)
+    (hp : p ≠ s.endValidPos) : (p.modify f hp).ValidPos :=
   p.pastSet _ _
 
-theorem remainingBytes_pastModify {s : String} {p : s.Pos} {f : Char → Char} {hp} :
+theorem remainingBytes_pastModify {s : String} {p : s.ValidPos} {f : Char → Char} {hp} :
     (p.pastModify f hp).remainingBytes = (p.next hp).remainingBytes :=
   remainingBytes_pastSet
 
@@ -148,8 +148,8 @@ invalid, the string is returned unchanged.
 If both the replacement character and the replaced character are 7-bit ASCII characters and the
 string is not shared, then it is updated in-place and not copied.
 
-This is a legacy function. The recommended alternative is `String.Pos.set`, combined with
-`String.pos` or another means of obtaining a `String.Pos`.
+This is a legacy function. The recommended alternative is `String.ValidPos.set`, combined with
+`String.pos` or another means of obtaining a `String.ValidPos`.
 
 Examples:
 * `"abc".set ⟨1⟩ 'B' = "aBc"`
@@ -173,8 +173,8 @@ character. If `p` is an invalid position, the string is returned unchanged.
 If both the replacement character and the replaced character are 7-bit ASCII characters and the
 string is not shared, then it is updated in-place and not copied.
 
-This is a legacy function. The recommended alternative is `String.Pos.set`, combined with
-`String.pos` or another means of obtaining a `String.Pos`.
+This is a legacy function. The recommended alternative is `String.ValidPos.set`, combined with
+`String.pos` or another means of obtaining a `String.ValidPos`.
 
 Examples:
 * `"abc".modify ⟨1⟩ Char.toUpper = "aBc"`
@@ -188,14 +188,14 @@ def Pos.Raw.modify (s : String) (i : Pos.Raw) (f : Char → Char) : String :=
 def modify (s : String) (i : Pos.Raw) (f : Char → Char) : String :=
   i.set s (f (i.get s))
 
-@[specialize] def mapAux (f : Char → Char) (s : String) (p : s.Pos) : String :=
-  if h : p = s.endPos then
+@[specialize] def mapAux (f : Char → Char) (s : String) (p : s.ValidPos) : String :=
+  if h : p = s.endValidPos then
     s
   else
     mapAux f (p.modify f h) (p.pastModify f h)
 termination_by p.remainingBytes
 decreasing_by
-  simp [remainingBytes_pastModify, ← Pos.lt_iff_remainingBytes_lt]
+  simp [remainingBytes_pastModify, ← ValidPos.lt_iff_remainingBytes_lt]
 
 /--
 Applies the function `f` to every character in a string, returning a string that contains the
@@ -206,7 +206,7 @@ Examples:
  * `"".map Char.toUpper = ""`
 -/
 @[inline] def map (f : Char → Char) (s : String) : String :=
-  mapAux f s s.startPos
+  mapAux f s s.startValidPos
 
 /--
 Replaces each character in `s` with the result of applying `Char.toUpper` to it.

src/Init/Data/String/Pattern/Basic.lean

@@ -112,12 +112,12 @@ def memcmpSlice (lhs rhs : Slice) (lstart : String.Pos.Raw) (rstart : String.Pos
     (by
       have := lhs.startInclusive_le_endExclusive
       have := lhs.endExclusive.isValid.le_utf8ByteSize
-      simp [String.Pos.le_iff, Pos.Raw.le_iff, Slice.utf8ByteSize_eq] at *
+      simp [ValidPos.le_iff, Pos.Raw.le_iff, Slice.utf8ByteSize_eq] at *
       omega)
     (by
       have := rhs.startInclusive_le_endExclusive
       have := rhs.endExclusive.isValid.le_utf8ByteSize
-      simp [String.Pos.le_iff, Pos.Raw.le_iff, Slice.utf8ByteSize_eq] at *
+      simp [ValidPos.le_iff, Pos.Raw.le_iff, Slice.utf8ByteSize_eq] at *
       omega)
 
 end Internal

src/Init/Data/String/Pattern/Char.lean

@@ -21,44 +21,46 @@ public section
 
 namespace String.Slice.Pattern
 
-structure ForwardCharSearcher (needle : Char) (s : Slice) where
+structure ForwardCharSearcher (s : Slice) where
   currPos : s.Pos
+  needle : Char
 deriving Inhabited
 
 namespace ForwardCharSearcher
 
 @[inline]
-def iter (c : Char) (s : Slice) : Std.Iter (α := ForwardCharSearcher c s) (SearchStep s) :=
-  { internalState := { currPos := s.startPos }}
+def iter (c : Char) (s : Slice) : Std.Iter (α := ForwardCharSearcher s) (SearchStep s) :=
+  { internalState := { currPos := s.startPos, needle := c }}
 
-instance (s : Slice) : Std.Iterators.Iterator (ForwardCharSearcher c s) Id (SearchStep s) where
+instance (s : Slice) : Std.Iterators.Iterator (ForwardCharSearcher s) Id (SearchStep s) where
   IsPlausibleStep it
     | .yield it' out =>
+      it.internalState.needle = it'.internalState.needle ∧
       ∃ h1 : it.internalState.currPos ≠ s.endPos,
         it'.internalState.currPos = it.internalState.currPos.next h1 ∧
         match out with
         | .matched startPos endPos =>
           it.internalState.currPos = startPos ∧
           it'.internalState.currPos = endPos ∧
-          it.internalState.currPos.get h1 = c
+          it.internalState.currPos.get h1 = it.internalState.needle
         | .rejected startPos endPos =>
           it.internalState.currPos = startPos ∧
           it'.internalState.currPos = endPos ∧
-          it.internalState.currPos.get h1 ≠ c
+          it.internalState.currPos.get h1 ≠ it.internalState.needle
     | .skip _ => False
     | .done => it.internalState.currPos = s.endPos
-  step := fun ⟨⟨currPos⟩⟩ =>
+  step := fun ⟨currPos, needle⟩ =>
     if h1 : currPos = s.endPos then
       pure (.deflate ⟨.done, by simp [h1]⟩)
     else
       let nextPos := currPos.next h1
-      let nextIt := ⟨⟨nextPos⟩⟩
-      if h2 : currPos.get h1 = c then
+      let nextIt := ⟨nextPos, needle⟩
+      if h2 : currPos.get h1 = needle then
         pure (.deflate ⟨.yield nextIt (.matched currPos nextPos), by simp [h1, h2, nextIt, nextPos]⟩)
       else
         pure (.deflate ⟨.yield nextIt (.rejected currPos nextPos), by simp [h1, h2, nextIt, nextPos]⟩)
 
-def finitenessRelation : Std.Iterators.FinitenessRelation (ForwardCharSearcher s c) Id where
+def finitenessRelation : Std.Iterators.FinitenessRelation (ForwardCharSearcher s) Id where
   rel := InvImage WellFoundedRelation.rel (fun it => it.internalState.currPos)
   wf := InvImage.wf _ WellFoundedRelation.wf
   subrelation {it it'} h := by
@@ -66,18 +68,18 @@ def finitenessRelation : Std.Iterators.FinitenessRelation (ForwardCharSearcher s
     obtain ⟨step, h, h'⟩ := h
     cases step
     · cases h
-      obtain ⟨_, h2, _⟩ := h'
+      obtain ⟨_, h1, h2, _⟩ := h'
       simp [h2]
     · cases h'
     · cases h
 
-instance : Std.Iterators.Finite (ForwardCharSearcher s c) Id :=
+instance : Std.Iterators.Finite (ForwardCharSearcher s) Id :=
   .of_finitenessRelation finitenessRelation
 
-instance : Std.Iterators.IteratorLoop (ForwardCharSearcher s c) Id Id :=
+instance : Std.Iterators.IteratorLoop (ForwardCharSearcher s) Id Id :=
   .defaultImplementation
 
-instance {c : Char} : ToForwardSearcher c (ForwardCharSearcher c) where
+instance {c : Char} : ToForwardSearcher c ForwardCharSearcher where
   toSearcher := iter c
 
 instance {c : Char} : ForwardPattern c := .defaultImplementation

src/Init/Data/String/Pattern/Pred.lean

@@ -22,45 +22,47 @@ public section
 
 namespace String.Slice.Pattern
 
-structure ForwardCharPredSearcher (p : Char → Bool) (s : Slice) where
+structure ForwardCharPredSearcher (s : Slice) where
   currPos : s.Pos
+  needle : Char → Bool
 deriving Inhabited
 
 namespace ForwardCharPredSearcher
 
 @[inline]
-def iter (p : Char → Bool) (s : Slice) : Std.Iter (α := ForwardCharPredSearcher p s) (SearchStep s) :=
-  { internalState := { currPos := s.startPos }}
+def iter (p : Char → Bool) (s : Slice) : Std.Iter (α := ForwardCharPredSearcher s) (SearchStep s) :=
+  { internalState := { currPos := s.startPos, needle := p }}
 
-instance (s : Slice) : Std.Iterators.Iterator (ForwardCharPredSearcher p s) Id (SearchStep s) where
+instance (s : Slice) : Std.Iterators.Iterator (ForwardCharPredSearcher s) Id (SearchStep s) where
   IsPlausibleStep it
     | .yield it' out =>
+      it.internalState.needle = it'.internalState.needle ∧
       ∃ h1 : it.internalState.currPos ≠ s.endPos,
         it'.internalState.currPos = it.internalState.currPos.next h1 ∧
         match out with
         | .matched startPos endPos =>
           it.internalState.currPos = startPos ∧
           it'.internalState.currPos = endPos ∧
-          p (it.internalState.currPos.get h1)
+          it.internalState.needle (it.internalState.currPos.get h1)
         | .rejected startPos endPos =>
           it.internalState.currPos = startPos ∧
           it'.internalState.currPos = endPos ∧
-          ¬ p (it.internalState.currPos.get h1)
+          ¬ it.internalState.needle (it.internalState.currPos.get h1)
     | .skip _ => False
     | .done => it.internalState.currPos = s.endPos
-  step := fun ⟨⟨currPos⟩⟩ =>
+  step := fun ⟨currPos, needle⟩ =>
     if h1 : currPos = s.endPos then
       pure (.deflate ⟨.done, by simp [h1]⟩)
     else
       let nextPos := currPos.next h1
-      let nextIt := ⟨⟨nextPos⟩⟩
-      if h2 : p <| currPos.get h1 then
+      let nextIt := ⟨nextPos, needle⟩
+      if h2 : needle <| currPos.get h1 then
         pure (.deflate ⟨.yield nextIt (.matched currPos nextPos), by simp [h1, h2, nextPos, nextIt]⟩)
       else
         pure (.deflate ⟨.yield nextIt (.rejected currPos nextPos), by simp [h1, h2, nextPos, nextIt]⟩)
 
 
-def finitenessRelation : Std.Iterators.FinitenessRelation (ForwardCharPredSearcher p s) Id where
+def finitenessRelation : Std.Iterators.FinitenessRelation (ForwardCharPredSearcher s) Id where
   rel := InvImage WellFoundedRelation.rel (fun it => it.internalState.currPos)
   wf := InvImage.wf _ WellFoundedRelation.wf
   subrelation {it it'} h := by
@@ -68,23 +70,23 @@ def finitenessRelation : Std.Iterators.FinitenessRelation (ForwardCharPredSearch
     obtain ⟨step, h, h'⟩ := h
     cases step
     · cases h
-      obtain ⟨_, h2, _⟩ := h'
+      obtain ⟨_, h1, h2, _⟩ := h'
       simp [h2]
     · cases h'
     · cases h
 
-instance : Std.Iterators.Finite (ForwardCharPredSearcher p s) Id :=
+instance : Std.Iterators.Finite (ForwardCharPredSearcher s) Id :=
   .of_finitenessRelation finitenessRelation
 
-instance : Std.Iterators.IteratorLoop (ForwardCharPredSearcher p s) Id Id :=
+instance : Std.Iterators.IteratorLoop (ForwardCharPredSearcher s) Id Id :=
   .defaultImplementation
 
-instance {p : Char → Bool} : ToForwardSearcher p (ForwardCharPredSearcher p) where
+instance {p : Char → Bool} : ToForwardSearcher p ForwardCharPredSearcher where
   toSearcher := iter p
 
 instance {p : Char → Bool} : ForwardPattern p := .defaultImplementation
 
-instance {p : Char → Prop} [DecidablePred p] : ToForwardSearcher p (ForwardCharPredSearcher p) where
+instance {p : Char → Prop} [DecidablePred p] : ToForwardSearcher p ForwardCharPredSearcher where
   toSearcher := iter (decide <| p ·)
 
 instance {p : Char → Prop} [DecidablePred p] : ForwardPattern p :=

src/Init/Data/String/PosRaw.lean

@@ -108,7 +108,7 @@ At runtime, this function is implemented by efficient, constant-time code.
 -/
 @[extern "lean_string_get_byte_fast", expose]
 def getUTF8Byte (s : @& String) (p : Pos.Raw) (h : p < s.rawEndPos) : UInt8 :=
-  s.toByteArray[p.byteIdx]
+  s.bytes[p.byteIdx]
 
 @[deprecated getUTF8Byte (since := "2025-10-01"), extern "lean_string_get_byte_fast", expose]
 abbrev getUtf8Byte (s : String) (p : Pos.Raw) (h : p < s.rawEndPos) : UInt8 :=
@@ -216,7 +216,7 @@ theorem Pos.Raw.increaseBy_charUtf8Size {p : Pos.Raw} {c : Char} :
     p.increaseBy c.utf8Size = p + c := by
   simp [Pos.Raw.ext_iff]
 
-/-- Increases the byte offset of the position by `1`. Not to be confused with `Pos.next`. -/
+/-- Increases the byte offset of the position by `1`. Not to be confused with `ValidPos.next`. -/
 @[inline, expose]
 def Pos.Raw.inc (p : Pos.Raw) : Pos.Raw :=
   ⟨p.byteIdx + 1⟩
@@ -224,7 +224,7 @@ def Pos.Raw.inc (p : Pos.Raw) : Pos.Raw :=
 @[simp]
 theorem Pos.Raw.byteIdx_inc {p : Pos.Raw} : p.inc.byteIdx = p.byteIdx + 1 := (rfl)
 
-/-- Decreases the byte offset of the position by `1`. Not to be confused with `Pos.prev`. -/
+/-- Decreases the byte offset of the position by `1`. Not to be confused with `ValidPos.prev`. -/
 @[inline, expose]
 def Pos.Raw.dec (p : Pos.Raw) : Pos.Raw :=
   ⟨p.byteIdx - 1⟩

src/Init/Data/String/Repr.lean

@@ -0,0 +1,89 @@
+/-
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Leonardo de Moura, Mario Carneiro
+-/
+module
+
+prelude
+public import Init.Data.String.Substring
+import Init.Data.String.Search
+
+public section
+
+/--
+Interprets a string as the decimal representation of an integer, returning it. Returns `none` if
+the string does not contain a decimal integer.
+
+A string can be interpreted as a decimal integer if it only consists of at least one decimal digit
+and optionally `-` in front. Leading `+` characters are not allowed.
+
+Use `String.isInt` to check whether `String.toInt?` would return `some`. `String.toInt!` is an
+alternative that panics instead of returning `none` when the string is not an integer.
+
+Examples:
+ * `"".toInt? = none`
+ * `"-".toInt? = none`
+ * `"0".toInt? = some 0`
+ * `"5".toInt? = some 5`
+ * `"-5".toInt? = some (-5)`
+ * `"587".toInt? = some 587`
+ * `"-587".toInt? = some (-587)`
+ * `" 5".toInt? = none`
+ * `"2-3".toInt? = none`
+ * `"0xff".toInt? = none`
+-/
+def String.toInt? (s : String) : Option Int := do
+  if s.front = '-' then do
+    let v ← (s.toRawSubstring.drop 1).toNat?;
+    pure <| - Int.ofNat v
+  else
+   Int.ofNat <$> s.toNat?
+
+/--
+Checks whether the string can be interpreted as the decimal representation of an integer.
+
+A string can be interpreted as a decimal integer if it only consists of at least one decimal digit
+and optionally `-` in front. Leading `+` characters are not allowed.
+
+Use `String.toInt?` or `String.toInt!` to convert such a string to an integer.
+
+Examples:
+ * `"".isInt = false`
+ * `"-".isInt = false`
+ * `"0".isInt = true`
+ * `"-0".isInt = true`
+ * `"5".isInt = true`
+ * `"587".isInt = true`
+ * `"-587".isInt = true`
+ * `"+587".isInt = false`
+ * `" 5".isInt = false`
+ * `"2-3".isInt = false`
+ * `"0xff".isInt = false`
+-/
+def String.isInt (s : String) : Bool :=
+  if s.front = '-' then
+    (s.toRawSubstring.drop 1).isNat
+  else
+    s.isNat
+
+/--
+Interprets a string as the decimal representation of an integer, returning it. Panics if the string
+does not contain a decimal integer.
+
+A string can be interpreted as a decimal integer if it only consists of at least one decimal digit
+and optionally `-` in front. Leading `+` characters are not allowed.
+
+Use `String.isInt` to check whether `String.toInt!` would return a value. `String.toInt?` is a safer
+alternative that returns `none` instead of panicking when the string is not an integer.
+
+Examples:
+ * `"0".toInt! = 0`
+ * `"5".toInt! = 5`
+ * `"587".toInt! = 587`
+ * `"-587".toInt! = -587`
+-/
+def String.toInt! (s : String) : Int :=
+  match s.toInt? with
+  | some v => v
+  | none   => panic "Int expected"

src/Init/Data/String/Search.lean

@@ -88,28 +88,28 @@ Finds the position of the first match of the pattern {name}`pattern` in after th
 This function is generic over all currently supported patterns.
 
 Examples:
- * {lean}`("coffee tea water".startPos.find? Char.isWhitespace).map (·.get!) == some ' '`
+ * {lean}`("coffee tea water".startValidPos.find? Char.isWhitespace).map (·.get!) == some ' '`
  * {lean}`("tea".pos ⟨1⟩ (by decide)).find? (fun (c : Char) => c == 't') == none`
 -/
 @[inline]
-def Pos.find?  {s : String} (pos : s.Pos) (pattern : ρ)
-    [ToForwardSearcher pattern σ] : Option s.Pos :=
-  (pos.toSlice.find? pattern).map Pos.ofToSlice
+def ValidPos.find?  {s : String} (pos : s.ValidPos) (pattern : ρ)
+    [ToForwardSearcher pattern σ] : Option s.ValidPos :=
+  (pos.toSlice.find? pattern).map (·.ofSlice)
 
 /--
 Finds the position of the first match of the pattern {name}`pattern` in after the position
-{name}`pos`. If there is no match {lean}`s.endPos` is returned.
+{name}`pos`. If there is no match {lean}`s.endValidPos` is returned.
 
 This function is generic over all currently supported patterns.
 
 Examples:
- * {lean}`("coffee tea water".startPos.find Char.isWhitespace).get! == ' '`
- * {lean}`("tea".pos ⟨1⟩ (by decide)).find (fun (c : Char) => c == 't') == "tea".endPos`
+ * {lean}`("coffee tea water".startValidPos.find Char.isWhitespace).get! == ' '`
+ * {lean}`("tea".pos ⟨1⟩ (by decide)).find (fun (c : Char) => c == 't') == "tea".endValidPos`
 -/
 @[inline]
-def Pos.find {s : String} (pos : s.Pos) (pattern : ρ) [ToForwardSearcher pattern σ] :
-    s.Pos :=
-  ofToSlice (pos.toSlice.find pattern)
+def ValidPos.find {s : String} (pos : s.ValidPos) (pattern : ρ) [ToForwardSearcher pattern σ] :
+    s.ValidPos :=
+  (pos.toSlice.find pattern).ofSlice
 
 /--
 Finds the position of the first match of the pattern {name}`pattern` in a string {name}`s`. If
@@ -123,23 +123,23 @@ Examples:
  * {lean}`("coffee tea water".find? "tea").map (·.get!) == some 't'`
 -/
 @[inline]
-def find? (s : String) (pattern : ρ) [ToForwardSearcher pattern σ] : Option s.Pos :=
-  s.startPos.find? pattern
+def find? (s : String) (pattern : ρ) [ToForwardSearcher pattern σ] : Option s.ValidPos :=
+  s.startValidPos.find? pattern
 
 /--
 Finds the position of the first match of the pattern {name}`pattern` in a slice {name}`s`. If there
-is no match {lean}`s.endPos` is returned.
+is no match {lean}`s.endValidPos` is returned.
 
 This function is generic over all currently supported patterns.
 
 Examples:
  * {lean}`("coffee tea water".find Char.isWhitespace).get! == ' '`
- * {lean}`"tea".find (fun (c : Char) => c == 'X') == "tea".endPos`
+ * {lean}`"tea".find (fun (c : Char) => c == 'X') == "tea".endValidPos`
  * {lean}`("coffee tea water".find "tea").get! == 't'`
 -/
 @[inline]
-def find (s : String) (pattern : ρ) [ToForwardSearcher pattern σ] : s.Pos :=
-  s.startPos.find pattern
+def find (s : String) (pattern : ρ) [ToForwardSearcher pattern σ] : s.ValidPos :=
+  s.startValidPos.find pattern
 
 /--
 Finds the position of the first match of the pattern {name}`pattern` in a slice {name}`s` that is
@@ -166,13 +166,13 @@ This function is generic over all currently supported patterns except
 {name}`String`/{name}`String.Slice`.
 
 Examples:
-* {lean}`(("ab1c".endPos.prev (by decide)).revFind? Char.isAlpha).map (·.get!) == some 'b'`
-* {lean}`"abc".startPos.revFind? Char.isAlpha == none`
+* {lean}`(("ab1c".endValidPos.prev (by decide)).revFind? Char.isAlpha).map (·.get!) == some 'b'`
+* {lean}`"abc".startValidPos.revFind? Char.isAlpha == none`
 -/
 @[inline]
-def Pos.revFind? {s : String} (pos : s.Pos) (pattern : ρ) [ToBackwardSearcher pattern σ] :
-    Option s.Pos :=
-  (pos.toSlice.revFind? pattern).map Pos.ofToSlice
+def ValidPos.revFind? {s : String} (pos : s.ValidPos) (pattern : ρ) [ToBackwardSearcher pattern σ] :
+    Option s.ValidPos :=
+  (pos.toSlice.revFind? pattern).map (·.ofSlice)
 
 /--
 Finds the position of the first match of the pattern {name}`pattern` in a string, starting
@@ -187,32 +187,32 @@ Examples:
  * {lean}`"tea".toSlice.revFind? (fun (c : Char) => c == 'X') == none`
 -/
 @[inline]
-def revFind? (s : String) (pattern : ρ) [ToBackwardSearcher pattern σ] : Option s.Pos :=
-  s.endPos.revFind? pattern
+def revFind? (s : String) (pattern : ρ) [ToBackwardSearcher pattern σ] : Option s.ValidPos :=
+  s.endValidPos.revFind? pattern
 
 @[export lean_string_posof]
 def Internal.posOfImpl (s : String) (c : Char) : Pos.Raw :=
   (s.find c).offset
 
-@[deprecated String.Pos.find (since := "2025-11-19")]
+@[deprecated String.ValidPos.find (since := "2025-11-19")]
 def findAux (s : String) (p : Char → Bool) (stopPos : Pos.Raw) (pos : Pos.Raw) : Pos.Raw :=
   if h : pos ≤ stopPos ∧ pos.IsValid s ∧ stopPos.IsValid s then
     (String.Slice.mk s (s.pos pos h.2.1) (s.pos stopPos h.2.2)
-      (by simp [Pos.le_iff, h.1])).find p |>.str.offset
+      (by simp [ValidPos.le_iff, h.1])).find p |>.str.offset
   else stopPos
 
-@[deprecated String.Pos.find (since := "2025-11-19")]
+@[deprecated String.ValidPos.find (since := "2025-11-19")]
 def posOfAux (s : String) (c : Char) (stopPos : Pos.Raw) (pos : Pos.Raw) : Pos.Raw :=
   if h : pos ≤ stopPos ∧ pos.IsValid s ∧ stopPos.IsValid s then
     (String.Slice.mk s (s.pos pos h.2.1) (s.pos stopPos h.2.2)
-      (by simp [Pos.le_iff, h.1])).find c |>.str.offset
+      (by simp [ValidPos.le_iff, h.1])).find c |>.str.offset
   else stopPos
 
 @[deprecated String.find (since := "2025-11-19")]
 def posOf (s : String) (c : Char) : Pos.Raw :=
   (s.find c).offset
 
-@[deprecated String.Pos.revFind? (since := "2025-11-19")]
+@[deprecated String.ValidPos.revFind? (since := "2025-11-19")]
 def revPosOfAux (s : String) (c : Char) (pos : Pos.Raw) : Option Pos.Raw :=
   s.pos? pos |>.bind (·.revFind? c) |>.map (·.offset)
 
@@ -220,7 +220,7 @@ def revPosOfAux (s : String) (c : Char) (pos : Pos.Raw) : Option Pos.Raw :=
 def revPosOf (s : String) (c : Char) : Option Pos.Raw :=
   s.revFind? c |>.map (·.offset)
 
-@[deprecated String.Pos.revFind? (since := "2025-11-19")]
+@[deprecated String.ValidPos.revFind? (since := "2025-11-19")]
 def revFindAux (s : String) (p : Char → Bool) (pos : Pos.Raw) : Option Pos.Raw :=
   s.pos? pos |>.bind (·.revFind? p) |>.map (·.offset)
 
@@ -234,9 +234,9 @@ Returns the position of the beginning of the line that contains the position {na
 Lines are ended by {lean}`'\n'`, and the returned position is either {lean}`0 : String.Pos.Raw` or
 immediately after a {lean}`'\n'` character.
 -/
-@[deprecated String.Pos.revFind? (since := "2025-11-19")]
+@[deprecated String.ValidPos.revFind? (since := "2025-11-19")]
 def findLineStart (s : String) (pos : String.Pos.Raw) : String.Pos.Raw :=
-  s.pos? pos |>.bind (·.revFind? '\n') |>.map (·.offset) |>.getD s.startPos.offset
+  s.pos? pos |>.bind (·.revFind? '\n') |>.map (·.offset) |>.getD s.startValidPos.offset
 
 /--
 Splits a string at each subslice that matches the pattern {name}`pat`.
@@ -293,68 +293,6 @@ Examples:
 def Internal.foldlImpl (f : String → Char → String) (init : String) (s : String) : String :=
   String.foldl f init s
 
-@[deprecated String.Slice.foldr (since := "2025-11-25")]
-def foldrAux {α : Type u} (f : Char → α → α) (a : α) (s : String) (i begPos : Pos.Raw) : α :=
-  s.slice! (s.pos! begPos) (s.pos! i) |>.foldr f a
-
-/--
-Folds a function over a string from the right, accumulating a value starting with {lean}`init`. The
-accumulated value is combined with each character in reverse order, using {lean}`f`.
-
-Examples:
- * {lean}`"coffee tea water".foldr (fun c n => if c.isWhitespace then n + 1 else n) 0 = 2`
- * {lean}`"coffee tea and water".foldr (fun c n => if c.isWhitespace then n + 1 else n) 0 = 3`
- * {lean}`"coffee tea water".foldr (fun c s => s.push c) "" = "retaw aet eeffoc"`
--/
-@[inline] def foldr {α : Type u} (f : Char → α → α) (init : α) (s : String) : α :=
-  s.toSlice.foldr f init
-
-@[deprecated String.Slice.any (since := "2025-11-25")]
-def anyAux (s : String) (stopPos : Pos.Raw) (p : Char → Bool) (i : Pos.Raw) : Bool :=
-  s.slice! (s.pos! i) (s.pos! stopPos) |>.any p
-
-
-/--
-Checks whether a string has a match of the pattern {name}`pat` anywhere.
-
-This function is generic over all currently supported patterns.
-
-Examples:
- * {lean}`"coffee tea water".contains Char.isWhitespace = true`
- * {lean}`"tea".contains (fun (c : Char) => c == 'X') = false`
- * {lean}`"coffee tea water".contains "tea" = true`
--/
-@[inline] def contains (s : String) (pat : ρ) [ToForwardSearcher pat σ] : Bool :=
-  s.toSlice.contains pat
-
-@[export lean_string_contains]
-def Internal.containsImpl (s : String) (c : Char) : Bool :=
-  String.contains s c
-
-@[inline, inherit_doc contains] def any (s : String) (pat : ρ) [ToForwardSearcher pat σ] : Bool :=
-  s.contains pat
-
-@[export lean_string_any]
-def Internal.anyImpl (s : String) (p : Char → Bool) :=
-  String.any s p
-
-/--
-Checks whether a slice only consists of matches of the pattern {name}`pat`.
-
-Short-circuits at the first pattern mis-match.
-
-This function is generic over all currently supported patterns.
-
-Examples:
- * {lean}`"brown".all Char.isLower = true`
- * {lean}`"brown and orange".all Char.isLower = false`
- * {lean}`"aaaaaa".all 'a' = true`
- * {lean}`"aaaaaa".all "aa" = true`
- * {lean}`"aaaaaaa".all "aa" = false`
--/
-@[inline] def all (s : String) (pat : ρ) [ForwardPattern pat] : Bool :=
-  s.toSlice.all pat
-
 /--
 Checks whether the string can be interpreted as the decimal representation of a natural number.
 
@@ -420,78 +358,6 @@ Examples:
 @[inline] def toNat! (s : String) : Nat :=
   s.toSlice.toNat!
 
-/--
-Interprets a string as the decimal representation of an integer, returning it. Returns {lean}`none`
-if the string does not contain a decimal integer.
-
-A string can be interpreted as a decimal integer if it only consists of at least one decimal digit
-and optionally {lit}`-` in front. Leading `+` characters are not allowed.
-
-Use {name (scope := "Init.Data.String.Search")}`String.isInt` to check whether {name}`String.toInt?`
-would return {lean}`some`. {name (scope := "Init.Data.String.Search")}`String.toInt!` is an
-alternative that panics instead of returning {lean}`none` when the string is not an integer.
-
-Examples:
- * {lean}`"".toInt? = none`
- * {lean}`"-".toInt? = none`
- * {lean}`"0".toInt? = some 0`
- * {lean}`"5".toInt? = some 5`
- * {lean}`"-5".toInt? = some (-5)`
- * {lean}`"587".toInt? = some 587`
- * {lean}`"-587".toInt? = some (-587)`
- * {lean}`" 5".toInt? = none`
- * {lean}`"2-3".toInt? = none`
- * {lean}`"0xff".toInt? = none`
--/
-@[inline] def toInt? (s : String) : Option Int :=
-  s.toSlice.toInt?
-
-/--
-Checks whether the string can be interpreted as the decimal representation of an integer.
-
-A string can be interpreted as a decimal integer if it only consists of at least one decimal digit
-and optionally {lit}`-` in front. Leading `+` characters are not allowed.
-
-Use {name}`String.toInt?` or {name (scope := "Init.Data.String.Search")}`String.toInt!` to convert
-such a string to an integer.
-
-Examples:
- * {lean}`"".isInt = false`
- * {lean}`"-".isInt = false`
- * {lean}`"0".isInt = true`
- * {lean}`"-0".isInt = true`
- * {lean}`"5".isInt = true`
- * {lean}`"587".isInt = true`
- * {lean}`"-587".isInt = true`
- * {lean}`"+587".isInt = false`
- * {lean}`" 5".isInt = false`
- * {lean}`"2-3".isInt = false`
- * {lean}`"0xff".isInt = false`
--/
-@[inline] def isInt (s : String) : Bool :=
-  s.toSlice.isInt
-
-/--
-Interprets a string as the decimal representation of an integer, returning it. Panics if the string
-does not contain a decimal integer.
-
-A string can be interpreted as a decimal integer if it only consists of at least one decimal digit
-and optionally {lit}`-` in front. Leading `+` characters are not allowed.
-
-Use {name}`String.isInt` to check whether {name}`String.toInt!` would return a value.
-{name}`String.toInt?` is a safer alternative that returns {lean}`none` instead of panicking when the
-string is not an integer.
-
-Examples:
- * {lean}`"0".toInt! = 0`
- * {lean}`"5".toInt! = 5`
- * {lean}`"587".toInt! = 587`
- * {lean}`"-587".toInt! = -587`
--/
-@[inline] def toInt! (s : String) : Int :=
-  s.toSlice.toInt!
-
-
 /--
 Returns the first character in {name}`s`. If {name}`s` is empty, returns {name}`none`.
 
@@ -539,14 +405,14 @@ Examples:
 @[inline, expose] def back (s : String) : Char :=
   s.toSlice.back
 
-theorem Pos.ofToSlice_ne_endPos {s : String} {p : s.toSlice.Pos}
-    (h : p ≠ s.toSlice.endPos) : ofToSlice p ≠ s.endPos := by
-  rwa [ne_eq, ← Pos.toSlice_inj, Slice.Pos.toSlice_ofToSlice, ← endPos_toSlice]
+theorem Slice.Pos.ofSlice_ne_endValidPos {s : String} {p : s.toSlice.Pos}
+    (h : p ≠ s.toSlice.endPos) : p.ofSlice ≠ s.endValidPos := by
+  rwa [ne_eq, ← ValidPos.toSlice_inj, toSlice_ofSlice, ← endPos_toSlice]
 
 @[inline]
 def Internal.toSliceWithProof {s : String} :
-    { p : s.toSlice.Pos // p ≠ s.toSlice.endPos } → { p : s.Pos // p ≠ s.endPos } :=
-  fun ⟨p, h⟩ => ⟨Pos.ofToSlice p, Pos.ofToSlice_ne_endPos h⟩
+    { p : s.toSlice.Pos // p ≠ s.toSlice.endPos } → { p : s.ValidPos // p ≠ s.endValidPos } :=
+  fun ⟨p, h⟩ => ⟨p.ofSlice, Slice.Pos.ofSlice_ne_endValidPos h⟩
 
 /--
 Creates an iterator over all valid positions within {name}`s`.
@@ -559,7 +425,7 @@ Examples
 -/
 @[inline]
 def positions (s : String) :=
-  (s.toSlice.positions.map Internal.toSliceWithProof : Std.Iter { p : s.Pos // p ≠ s.endPos })
+  (s.toSlice.positions.map Internal.toSliceWithProof : Std.Iter { p : s.ValidPos // p ≠ s.endValidPos })
 
 /--
 Creates an iterator over all characters (Unicode code points) in {name}`s`.
@@ -584,7 +450,7 @@ Examples
 -/
 @[inline]
 def revPositions (s : String) :=
-  (s.toSlice.revPositions.map Internal.toSliceWithProof : Std.Iter { p : s.Pos // p ≠ s.endPos })
+  (s.toSlice.revPositions.map Internal.toSliceWithProof : Std.Iter { p : s.ValidPos // p ≠ s.endValidPos })
 
 /--
 Creates an iterator over all characters (Unicode code points) in {name}`s`, starting from the end

src/Init/Data/String/Slice.lean

@@ -529,7 +529,7 @@ def any (s : Slice) (pat : ρ) [ToForwardSearcher pat σ] : Bool :=
   s.contains pat
 
 /--
-Checks whether a slice only consists of matches of the pattern {name}`pat`.
+Checks whether a slice only consists of matches of the pattern {name}`pat` anywhere.
 
 Short-circuits at the first pattern mis-match.
 
@@ -1339,85 +1339,6 @@ Examples:
 def front (s : Slice) : Char :=
   s.front?.getD default
 
-/--
-Checks whether the slice can be interpreted as the decimal representation of an integer.
-
-A slice can be interpreted as a decimal integer if it only consists of at least one decimal digit
-and optionally {lit}`-` in front. Leading {lit}`+` characters are not allowed.
-
-Use {name (scope := "Init.Data.String.Slice")}`String.Slice.toInt?` or {name (scope := "Init.Data.String.Slice")}`String.toInt!` to convert such a string to an integer.
-
-Examples:
- * {lean}`"".toSlice.isInt = false`
- * {lean}`"-".toSlice.isInt = false`
- * {lean}`"0".toSlice.isInt = true`
- * {lean}`"-0".toSlice.isInt = true`
- * {lean}`"5".toSlice.isInt = true`
- * {lean}`"587".toSlice.isInt = true`
- * {lean}`"-587".toSlice.isInt = true`
- * {lean}`"+587".toSlice.isInt = false`
- * {lean}`" 5".toSlice.isInt = false`
- * {lean}`"2-3".toSlice.isInt = false`
- * {lean}`"0xff".toSlice.isInt = false`
--/
-def isInt (s : Slice) : Bool :=
-  if s.front = '-' then
-    (s.drop 1).isNat
-  else
-    s.isNat
-
-/--
-Interprets a slice as the decimal representation of an integer, returning it. Returns {lean}`none` if
-the string does not contain a decimal integer.
-
-A string can be interpreted as a decimal integer if it only consists of at least one decimal digit
-and optionally {lit}`-` in front. Leading {lit}`+` characters are not allowed.
-
-Use {name}`Slice.isInt` to check whether {name}`Slice.toInt?` would return {lean}`some`.
-{name (scope := "Init.Data.String.Slice")}`Slice.toInt!` is an alternative that panics instead of
-returning {lean}`none` when the string is not an integer.
-
-Examples:
- * {lean}`"".toSlice.toInt? = none`
- * {lean}`"-".toSlice.toInt? = none`
- * {lean}`"0".toSlice.toInt? = some 0`
- * {lean}`"5".toSlice.toInt? = some 5`
- * {lean}`"-5".toSlice.toInt? = some (-5)`
- * {lean}`"587".toSlice.toInt? = some 587`
- * {lean}`"-587".toSlice.toInt? = some (-587)`
- * {lean}`" 5".toSlice.toInt? = none`
- * {lean}`"2-3".toSlice.toInt? = none`
- * {lean}`"0xff".toSlice.toInt? = none`
--/
-def toInt? (s : Slice) : Option Int :=
-  if s.front = '-' then
-    Int.negOfNat <$> (s.drop 1).toNat?
-  else
-   Int.ofNat <$> s.toNat?
-
-/--
-Interprets a string as the decimal representation of an integer, returning it. Panics if the string
-does not contain a decimal integer.
-
-A string can be interpreted as a decimal integer if it only consists of at least one decimal digit
-and optionally {lit}`-` in front. Leading `+` characters are not allowed.
-
-Use {name}`Slice.isInt` to check whether {name}`Slice.toInt!` would return a value.
-{name}`Slice.toInt?` is a safer alternative that returns {lean}`none` instead of panicking when the
-string is not an integer.
-
-Examples:
- * {lean}`"0".toSlice.toInt! = 0`
- * {lean}`"5".toSlice.toInt! = 5`
- * {lean}`"587".toSlice.toInt! = 587`
- * {lean}`"-587".toSlice.toInt! = -587`
--/
-@[inline]
-def toInt! (s : Slice) : Int :=
-  match s.toInt? with
-  | some v => v
-  | none   => panic "Int expected"
-
 /--
 Returns the last character in {name}`s`. If {name}`s` is empty, returns {name}`none`.
 

src/Init/Data/String/Substring.lean

@@ -32,10 +32,10 @@ def ofSlice (s : String.Slice) : Substring.Raw where
 Converts a `Substring.Raw` into a `String.Slice`, returning `none` if the substring is invalid.
 -/
 @[inline]
-def toSlice? (s : Substring.Raw) : Option String.Slice :=
+def toSlice (s : Substring.Raw) : Option String.Slice :=
   if h : s.startPos.IsValid s.str ∧ s.stopPos.IsValid s.str ∧ s.startPos ≤ s.stopPos then
     some (String.Slice.mk s.str (s.str.pos s.startPos h.1) (s.str.pos s.stopPos h.2.1)
-      (by simp [String.Pos.le_iff, h.2.2]))
+      (by simp [String.ValidPos.le_iff, h.2.2]))
   else
     none
 
@@ -155,7 +155,7 @@ Returns the substring-relative position of the first occurrence of `c` in `s`, o
 doesn't occur.
 -/
 @[inline] def posOf (s : Substring.Raw) (c : Char) : String.Pos.Raw :=
-  s.toSlice?.map (·.find c |>.offset) |>.getD ⟨s.bsize⟩
+  s.toSlice.map (·.find c |>.offset) |>.getD ⟨s.bsize⟩
 
 /--
 Removes the specified number of characters (Unicode code points) from the beginning of a substring
@@ -260,14 +260,15 @@ Folds a function over a substring from the left, accumulating a value starting w
 accumulated value is combined with each character in order, using `f`.
 -/
 @[inline] def foldl {α : Type u} (f : α → Char → α) (init : α) (s : Substring.Raw) : α :=
-  s.toSlice?.get!.foldl f init
+  s.toSlice.get!.foldl f init
 
 /--
 Folds a function over a substring from the right, accumulating a value starting with `init`. The
 accumulated value is combined with each character in reverse order, using `f`.
 -/
 @[inline] def foldr {α : Type u} (f : Char → α → α) (init : α) (s : Substring.Raw) : α :=
-  s.toSlice?.get!.foldr f init
+  match s with
+  | ⟨s, b, e⟩ => String.foldrAux f init s e b
 
 /--
 Checks whether the Boolean predicate `p` returns `true` for any character in a substring.
@@ -275,7 +276,8 @@ Checks whether the Boolean predicate `p` returns `true` for any character in a s
 Short-circuits at the first character for which `p` returns `true`.
 -/
 @[inline] def any (s : Substring.Raw) (p : Char → Bool) : Bool :=
-  s.toSlice?.get!.any p
+  match s with
+  | ⟨s, b, e⟩ => String.anyAux s e p b
 
 /--
 Checks whether the Boolean predicate `p` returns `true` for every character in a substring.
@@ -283,7 +285,7 @@ Checks whether the Boolean predicate `p` returns `true` for every character in a
 Short-circuits at the first character for which `p` returns `false`.
 -/
 @[inline] def all (s : Substring.Raw) (p : Char → Bool) : Bool :=
-  s.toSlice?.get!.all p
+  !s.any (fun c => !p c)
 
 @[export lean_substring_all]
 def Internal.allImpl (s : Substring.Raw) (p : Char → Bool) : Bool :=

src/Init/Data/String/Termination.lean

@@ -113,119 +113,119 @@ theorem prev_prev_lt {s : Slice} {p : s.Pos} {h h'} : (p.prev h).prev h' < p :=
 
 end Slice.Pos
 
-namespace Pos
+namespace ValidPos
 
 /-- The number of bytes between `p` and the end position. This number decreases as `p` advances. -/
-def remainingBytes {s : String} (p : s.Pos) : Nat :=
+def remainingBytes {s : String} (p : s.ValidPos) : Nat :=
   p.toSlice.remainingBytes
 
 @[simp]
-theorem remainingBytes_toSlice {s : String} {p : s.Pos} :
+theorem remainingBytes_toSlice {s : String} {p : s.ValidPos} :
     p.toSlice.remainingBytes = p.remainingBytes := (rfl)
 
-theorem remainingBytes_eq_byteDistance {s : String} {p : s.Pos} :
-    p.remainingBytes = p.offset.byteDistance s.endPos.offset := (rfl)
+theorem remainingBytes_eq_byteDistance {s : String} {p : s.ValidPos} :
+    p.remainingBytes = p.offset.byteDistance s.endValidPos.offset := (rfl)
 
-theorem remainingBytes_eq {s : String} {p : s.Pos} :
+theorem remainingBytes_eq {s : String} {p : s.ValidPos} :
     p.remainingBytes = s.utf8ByteSize - p.offset.byteIdx := by
   simp [remainingBytes_eq_byteDistance, Pos.Raw.byteDistance_eq]
 
-theorem remainingBytes_inj {s : String} {p q : s.Pos} :
+theorem remainingBytes_inj {s : String} {p q : s.ValidPos} :
     p.remainingBytes = q.remainingBytes ↔ p = q := by
-  simp [← remainingBytes_toSlice, Pos.toSlice_inj, Slice.Pos.remainingBytes_inj]
+  simp [← remainingBytes_toSlice, ValidPos.toSlice_inj, Slice.Pos.remainingBytes_inj]
 
-theorem le_iff_remainingBytes_le {s : String} (p q : s.Pos) :
+theorem le_iff_remainingBytes_le {s : String} (p q : s.ValidPos) :
     p ≤ q ↔ q.remainingBytes ≤ p.remainingBytes := by
   simp [← remainingBytes_toSlice, ← Slice.Pos.le_iff_remainingBytes_le]
 
-theorem lt_iff_remainingBytes_lt {s : String} (p q : s.Pos) :
+theorem lt_iff_remainingBytes_lt {s : String} (p q : s.ValidPos) :
     p < q ↔ q.remainingBytes < p.remainingBytes := by
   simp [← remainingBytes_toSlice, ← Slice.Pos.lt_iff_remainingBytes_lt]
 
-theorem wellFounded_lt {s : String} : WellFounded (fun (p : s.Pos) q => p < q) := by
+theorem wellFounded_lt {s : String} : WellFounded (fun (p : s.ValidPos) q => p < q) := by
   simpa [lt_iff, Pos.Raw.lt_iff] using
-    InvImage.wf (Pos.Raw.byteIdx ∘ Pos.offset) Nat.lt_wfRel.wf
+    InvImage.wf (Pos.Raw.byteIdx ∘ ValidPos.offset) Nat.lt_wfRel.wf
 
-theorem wellFounded_gt {s : String} : WellFounded (fun (p : s.Pos) q => q < p) := by
+theorem wellFounded_gt {s : String} : WellFounded (fun (p : s.ValidPos) q => q < p) := by
   simpa [lt_iff_remainingBytes_lt] using
-    InvImage.wf Pos.remainingBytes Nat.lt_wfRel.wf
+    InvImage.wf ValidPos.remainingBytes Nat.lt_wfRel.wf
 
-instance {s : String} : WellFoundedRelation s.Pos where
+instance {s : String} : WellFoundedRelation s.ValidPos where
   rel p q := q < p
-  wf := Pos.wellFounded_gt
+  wf := ValidPos.wellFounded_gt
 
-/-- Type alias for `String.Pos` representing that the given position is expected to decrease
+/-- Type alias for `String.ValidPos` representing that the given position is expected to decrease
 in recursive calls. -/
 structure Down (s : String) : Type where
-  inner : s.Pos
+  inner : s.ValidPos
 
 /-- Use `termination_by pos.down` to signify that in a recursive call, the parameter `pos` is
 expected to decrease. -/
-def down {s : String} (p : s.Pos) : Pos.Down s where
+def down {s : String} (p : s.ValidPos) : ValidPos.Down s where
   inner := p
 
 @[simp]
-theorem inner_down {s : String} {p : s.Pos} : p.down.inner = p := (rfl)
+theorem inner_down {s : String} {p : s.ValidPos} : p.down.inner = p := (rfl)
 
-instance {s : String} : WellFoundedRelation (Pos.Down s) where
+instance {s : String} : WellFoundedRelation (ValidPos.Down s) where
   rel p q := p.inner < q.inner
-  wf := InvImage.wf Pos.Down.inner Pos.wellFounded_lt
+  wf := InvImage.wf ValidPos.Down.inner ValidPos.wellFounded_lt
 
-theorem map_toSlice_next? {s : String} {p : s.Pos} :
-    p.next?.map Pos.toSlice = p.toSlice.next? := by
+theorem map_toSlice_next? {s : String} {p : s.ValidPos} :
+    p.next?.map ValidPos.toSlice = p.toSlice.next? := by
   simp [next?]
 
-theorem map_toSlice_prev? {s : String} {p : s.Pos} :
-    p.prev?.map Pos.toSlice = p.toSlice.prev? := by
+theorem map_toSlice_prev? {s : String} {p : s.ValidPos} :
+    p.prev?.map ValidPos.toSlice = p.toSlice.prev? := by
   simp [prev?]
 
-theorem ne_endPos_of_next?_eq_some {s : String} {p q : s.Pos}
-    (h : p.next? = some q) : p ≠ s.endPos :=
-  ne_of_apply_ne Pos.toSlice (Slice.Pos.ne_endPos_of_next?_eq_some
-    (by simpa only [Pos.map_toSlice_next?, Option.map_some] using congrArg (·.map toSlice) h))
+theorem ne_endValidPos_of_next?_eq_some {s : String} {p q : s.ValidPos}
+    (h : p.next? = some q) : p ≠ s.endValidPos :=
+  ne_of_apply_ne ValidPos.toSlice (Slice.Pos.ne_endPos_of_next?_eq_some
+    (by simpa only [ValidPos.map_toSlice_next?, Option.map_some] using congrArg (·.map toSlice) h))
 
-theorem eq_next_of_next?_eq_some {s : String} {p q : s.Pos} (h : p.next? = some q) :
-    q = p.next (ne_endPos_of_next?_eq_some h) := by
+theorem eq_next_of_next?_eq_some {s : String} {p q : s.ValidPos} (h : p.next? = some q) :
+    q = p.next (ne_endValidPos_of_next?_eq_some h) := by
   simpa only [← toSlice_inj, toSlice_next] using Slice.Pos.eq_next_of_next?_eq_some
-    (by simpa [Pos.map_toSlice_next?] using congrArg (·.map toSlice) h)
+    (by simpa [ValidPos.map_toSlice_next?] using congrArg (·.map toSlice) h)
 
-theorem ne_startPos_of_prev?_eq_some {s : String} {p q : s.Pos}
-    (h : p.prev? = some q) : p ≠ s.startPos :=
-  ne_of_apply_ne Pos.toSlice (Slice.Pos.ne_startPos_of_prev?_eq_some
-    (by simpa only [Pos.map_toSlice_prev?, Option.map_some] using congrArg (·.map toSlice) h))
+theorem ne_startValidPos_of_prev?_eq_some {s : String} {p q : s.ValidPos}
+    (h : p.prev? = some q) : p ≠ s.startValidPos :=
+  ne_of_apply_ne ValidPos.toSlice (Slice.Pos.ne_startPos_of_prev?_eq_some
+    (by simpa only [ValidPos.map_toSlice_prev?, Option.map_some] using congrArg (·.map toSlice) h))
 
-theorem eq_prev_of_prev?_eq_some {s : String} {p q : s.Pos} (h : p.prev? = some q) :
-    q = p.prev (ne_startPos_of_prev?_eq_some h) := by
+theorem eq_prev_of_prev?_eq_some {s : String} {p q : s.ValidPos} (h : p.prev? = some q) :
+    q = p.prev (ne_startValidPos_of_prev?_eq_some h) := by
   simpa only [← toSlice_inj, toSlice_prev] using Slice.Pos.eq_prev_of_prev?_eq_some
-    (by simpa [Pos.map_toSlice_prev?] using congrArg (·.map toSlice) h)
+    (by simpa [ValidPos.map_toSlice_prev?] using congrArg (·.map toSlice) h)
 
 @[simp]
-theorem le_refl {s : String} (p : s.Pos) : p ≤ p := by
-  simp [Pos.le_iff]
+theorem le_refl {s : String} (p : s.ValidPos) : p ≤ p := by
+  simp [ValidPos.le_iff]
 
-theorem lt_trans {s : String} {p q r : s.Pos} : p < q → q < r → p < r := by
-  simpa [Pos.lt_iff, Pos.Raw.lt_iff] using Nat.lt_trans
+theorem lt_trans {s : String} {p q r : s.ValidPos} : p < q → q < r → p < r := by
+  simpa [ValidPos.lt_iff, Pos.Raw.lt_iff] using Nat.lt_trans
 
 @[simp]
-theorem lt_next_next {s : String} {p : s.Pos} {h h'} : p < (p.next h).next h' :=
+theorem lt_next_next {s : String} {p : s.ValidPos} {h h'} : p < (p.next h).next h' :=
   lt_trans p.lt_next (p.next h).lt_next
 
 @[simp]
-theorem prev_prev_lt {s : String} {p : s.Pos} {h h'} : (p.prev h).prev h' < p :=
+theorem prev_prev_lt {s : String} {p : s.ValidPos} {h h'} : (p.prev h).prev h' < p :=
   lt_trans (p.prev h).prev_lt p.prev_lt
 
-theorem Splits.remainingBytes_eq {s : String} {p : s.Pos} {t₁ t₂}
+theorem Splits.remainingBytes_eq {s : String} {p : s.ValidPos} {t₁ t₂}
     (h : p.Splits t₁ t₂) : p.remainingBytes = t₂.utf8ByteSize := by
-  simp [Pos.remainingBytes_eq, h.eq_append, h.offset_eq_rawEndPos]
+  simp [ValidPos.remainingBytes_eq, h.eq_append, h.offset_eq_rawEndPos]
 
-end Pos
+end ValidPos
 
 namespace Slice.Pos
 
 @[simp]
 theorem remainingBytes_toCopy {s : Slice} {p : s.Pos} :
     p.toCopy.remainingBytes = p.remainingBytes := by
-  simp [remainingBytes_eq, String.Pos.remainingBytes_eq, Slice.utf8ByteSize_eq]
+  simp [remainingBytes_eq, ValidPos.remainingBytes_eq, Slice.utf8ByteSize_eq]
 
 theorem Splits.remainingBytes_eq {s : Slice} {p : s.Pos} {t₁ t₂} (h : p.Splits t₁ t₂) :
     p.remainingBytes = t₂.utf8ByteSize := by
@@ -244,14 +244,14 @@ macro_rules | `(tactic| decreasing_trivial) => `(tactic|
     Slice.Pos.eq_prev_of_prev?_eq_some (by assumption),
   ]) <;> done)
 macro_rules | `(tactic| decreasing_trivial) => `(tactic|
-  (with_reducible change (_ : String.Pos _) < _
+  (with_reducible change (_ : String.ValidPos _) < _
    simp [
-    Pos.eq_next_of_next?_eq_some (by assumption),
+    ValidPos.eq_next_of_next?_eq_some (by assumption),
   ]) <;> done)
 macro_rules | `(tactic| decreasing_trivial) => `(tactic|
-  (with_reducible change (_ : String.Pos _) < _
+  (with_reducible change (_ : String.ValidPos _) < _
    simp [
-    Pos.eq_prev_of_prev?_eq_some (by assumption),
+    ValidPos.eq_prev_of_prev?_eq_some (by assumption),
   ]) <;> done)
 
 end String

src/Init/Data/Vector/Basic.lean

@@ -525,12 +525,12 @@ and do not provide separate verification theorems.
 @[simp] theorem mem_toArray_iff (a : α) (xs : Vector α n) : a ∈ xs.toArray ↔ a ∈ xs :=
   ⟨fun h => ⟨h⟩, fun ⟨h⟩ => h⟩
 
-instance [Monad m] : ForIn' m (Vector α n) α inferInstance where
+instance : ForIn' m (Vector α n) α inferInstance where
   forIn' xs b f := Array.forIn' xs.toArray b (fun a h b => f a (by simpa using h) b)
 
 /-! ### ForM instance -/
 
-instance [Monad m] : ForM m (Vector α n) α where
+instance : ForM m (Vector α n) α where
   forM := Vector.forM
 
 -- We simplify `Vector.forM` to `forM`.

src/Init/GetElem.lean

@@ -116,7 +116,7 @@ macro:max x:term noWs "[" i:term "]" noWs "?" : term => `(getElem? $x $i)
 
 /--
 The syntax `arr[i]!` gets the `i`'th element of the collection `arr` and
-panics if `i` is out of bounds.
+panics `i` is out of bounds.
 -/
 macro:max x:term noWs "[" i:term "]" noWs "!" : term => `(getElem! $x $i)
 

src/Init/Grind.lean

@@ -27,4 +27,3 @@ public import Init.Grind.Order
 public import Init.Grind.Interactive
 public import Init.Grind.Lint
 public import Init.Grind.Annotated
-public import Init.Grind.FieldNormNum

src/Init/Grind/FieldNormNum.lean

@@ -1,219 +0,0 @@
-/-
-Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-module
-prelude
-public import Init.Grind.Ring.Field
-public import Init.Data.Rat.Basic
-import Init.Data.Rat.Lemmas
-public section
-namespace Lean.Grind.Field.NormNum
-
-attribute [local instance] Semiring.natCast Ring.intCast
-
-abbrev ofRat {α} [Field α] (r : Rat) : α :=
-  (r.num : α)/(r.den : α)
-
-attribute [local simp]
-  Field.inv_one Semiring.natCast_zero Semiring.natCast_one Ring.intCast_zero Ring.intCast_one Semiring.one_mul Semiring.mul_one
-  Semiring.pow_zero Field.inv_one Field.inv_zero
-
-private theorem dvd_helper₁ {z : Int} {n : Nat} : ↑(z.natAbs.gcd n : Int) ∣ z :=
-  Rat.normalize.dvd_num rfl
-private theorem dvd_helper₂ {z : Int} {n : Nat} : z.natAbs.gcd n ∣ n :=
-  Nat.gcd_dvd_right z.natAbs n
-
-private theorem nonzero_helper {α} [Field α] {z : Int} {n m : Nat} (hn : (n : α) ≠ 0) (hm : (m : α) ≠ 0) :
-    (z.natAbs.gcd (n * m) : α) ≠ 0 := by
-  intro h
-  have : z.natAbs.gcd (n * m) ∣ (n * m) := Nat.gcd_dvd_right z.natAbs (n * m)
-  obtain ⟨k, hk⟩ := this
-  replace hk := congrArg (fun x : Nat => (x : α)) hk
-  dsimp at hk
-  rw [Semiring.natCast_mul, Semiring.natCast_mul, h, Semiring.zero_mul] at hk
-  replace hk := Field.of_mul_eq_zero hk
-  simp_all
-
-theorem ofRat_add' {α} [Field α] {a b : Rat} (ha : (a.den : α) ≠ 0) (hb : (b.den : α) ≠ 0) :
-    (ofRat (a + b) : α) = ofRat a + ofRat b := by
-  rw [ofRat, ofRat, ofRat, Rat.num_add, Rat.den_add]
-  rw [Field.intCast_div_of_dvd dvd_helper₁ (by simpa [Ring.intCast_natCast] using (nonzero_helper ha hb))]
-  rw [Field.natCast_div_of_dvd dvd_helper₂ (nonzero_helper ha hb)]
-  rw [Ring.intCast_natCast, Field.div_div_right]
-  rw [Field.div_mul_cancel (nonzero_helper ha hb)]
-  rw [Field.add_div hb, Field.div_mul, Field.div_add ha]
-  rw [Ring.intCast_add, Ring.intCast_mul, Ring.intCast_mul, Ring.intCast_natCast,
-    Ring.intCast_natCast, CommSemiring.mul_comm (a.den : α), Field.div_div_left,
-    Semiring.natCast_mul]
-theorem ofRat_mul' {α} [Field α] {a b : Rat} (ha : (a.den : α) ≠ 0) (hb : (b.den : α) ≠ 0) : (ofRat (a * b) : α) = ofRat a * ofRat b := by
-  rw [ofRat, ofRat, ofRat, Rat.num_mul, Rat.den_mul]
-  rw [Field.intCast_div_of_dvd dvd_helper₁ (by simpa [Ring.intCast_natCast] using (nonzero_helper ha hb))]
-  rw [Field.natCast_div_of_dvd dvd_helper₂ (nonzero_helper ha hb)]
-  rw [Ring.intCast_natCast, Field.div_div_right]
-  rw [Field.div_mul_cancel (nonzero_helper ha hb)]
-  rw [Field.div_mul, Field.mul_div, Field.div_div_left, Ring.intCast_mul, Semiring.natCast_mul,
-    CommSemiring.mul_comm (b.den : α)]
-
--- Note: false without `IsCharP α 0` (consider `a = b = 1/2` in `ℤ/2ℤ`):
-theorem ofRat_add {α} [Field α] [IsCharP α 0] (a b : Rat) :
-    (ofRat (a + b) : α) = ofRat a + ofRat b :=
-  ofRat_add' (natCast_ne_zero a.den_nz) (natCast_ne_zero b.den_nz)
--- Note: false without `IsCharP α 0` (consider `a = 2/3` and `b = 1/2` in `ℤ/2ℤ`):
-theorem ofRat_mul {α} [Field α] [IsCharP α 0] (a b : Rat) : (ofRat (a * b) : α) = ofRat a * ofRat b :=
-  ofRat_mul' (natCast_ne_zero a.den_nz) (natCast_ne_zero b.den_nz)
-
-theorem ofRat_inv {α} [Field α] (a : Rat) : (ofRat (a⁻¹) : α) = (ofRat a)⁻¹ := by
-  simp [ofRat]; split
-  next h => simp [h, Field.div_eq_mul_inv]
-  next =>
-    simp [Field.div_eq_mul_inv, Field.inv_mul, Field.inv_inv, Ring.intCast_mul, Ring.intCast_natCast]
-    generalize a.num = n
-    generalize a.den = d
-    conv => rhs; rw [← Int.sign_mul_natAbs n]
-    simp [Ring.intCast_mul, Ring.intCast_natCast, Field.inv_mul]
-    have : (Int.cast n.sign : α) = (Int.cast n.sign : α)⁻¹ := by
-      cases Int.sign_trichotomy n
-      next h => simp [h]
-      next h => cases h <;> simp [*, Ring.intCast_neg, Field.inv_neg]
-    rw [← this, Semiring.mul_assoc, Semiring.mul_assoc]
-    congr 1
-    rw [CommSemiring.mul_comm]
-
-theorem ofRat_div' {α} [Field α] {a b : Rat} (ha : (a.den : α) ≠ 0) (hb : (b.num : α) ≠ 0) :
-    (ofRat (a / b) : α) = ofRat a / ofRat b := by
-  replace hb : ((b⁻¹).den : α) ≠ 0 := by
-    simp only [Rat.den_inv, Rat.num_eq_zero, ne_eq]
-    rw [if_neg (by intro h; simp_all)]
-    rw [← Ring.intCast_natCast]
-    by_cases h : 0 ≤ b.num
-    · have : (b.num.natAbs : Int) = b.num := Int.natAbs_of_nonneg h
-      rwa [this]
-    · have : (b.num.natAbs : Int) = -b.num := Int.ofNat_natAbs_of_nonpos (by omega)
-      rw [this, Ring.intCast_neg]
-      rwa [AddCommGroup.neg_eq_iff, AddCommGroup.neg_zero]
-  rw [Rat.div_def, ofRat_mul' ha hb, ofRat_inv, Field.div_eq_mul_inv (ofRat a)]
-
-theorem ofRat_div {α} [Field α] [IsCharP α 0] (a b : Rat) : (ofRat (a / b) : α) = ofRat a / ofRat b := by
-  rw [Rat.div_def, ofRat_mul, ofRat_inv, Field.div_eq_mul_inv (ofRat a)]
-
-theorem ofRat_neg {α} [Field α] (a : Rat) : (ofRat (-a) : α) = -ofRat a := by
-  simp [ofRat, Field.div_eq_mul_inv, Ring.intCast_neg, Ring.neg_mul]
-
-theorem ofRat_sub' {α} [Field α] {a b : Rat} (ha : (a.den : α) ≠ 0) (hb : (b.den : α) ≠ 0) :
-    (ofRat (a - b) : α) = ofRat a - ofRat b := by
-  replace hb : ((-b).den : α) ≠ 0 := by simpa
-  rw [Rat.sub_eq_add_neg, ofRat_add' ha hb, ofRat_neg, Ring.sub_eq_add_neg]
-
-theorem ofRat_sub {α} [Field α] [IsCharP α 0] (a b : Rat) :
-    (ofRat (a - b) : α) = ofRat a - ofRat b := by
-  rw [Rat.sub_eq_add_neg, ofRat_add, ofRat_neg, Ring.sub_eq_add_neg]
-
-theorem ofRat_npow' {α} [Field α] {a : Rat} (ha : (a.den : α) ≠ 0) (n : Nat) : (ofRat (a^n) : α) = ofRat a ^ n := by
-  have h : ∀ n : Nat, ((a^n).den : α) ≠ 0 := by
-    intro n
-    rw [Rat.den_pow, ne_eq, Semiring.natCast_pow]
-    intro h
-    induction n with
-    | zero =>
-      rw [Semiring.pow_zero] at h
-      exact Field.zero_ne_one h.symm
-    | succ n ih' =>
-      rw [Semiring.pow_succ] at h
-      replace h := Field.of_mul_eq_zero h
-      rcases h with h | h
-      · exact ih' h
-      · exact ha h
-  induction n
-  next => simp [Field.div_eq_mul_inv, ofRat]
-  next n ih =>
-    rw [Rat.pow_succ, ofRat_mul' (h _) ha, ih, Semiring.pow_succ]
-
-theorem ofRat_npow {α} [Field α] [IsCharP α 0] (a : Rat) (n : Nat) : (ofRat (a^n) : α) = ofRat a ^ n := by
-  induction n
-  next => simp [Field.div_eq_mul_inv, ofRat]
-  next n ih => rw [Rat.pow_succ, ofRat_mul, ih, Semiring.pow_succ]
-
-theorem ofRat_zpow' {α} [Field α] {a : Rat} (ha : (a.den : α) ≠ 0) (n : Int) : (ofRat (a^n) : α) = ofRat a ^ n := by
-  cases n
-  next => rw [Int.ofNat_eq_natCast, Rat.zpow_natCast, Field.zpow_natCast, ofRat_npow' ha]
-  next =>
-    rw [Int.negSucc_eq, Rat.zpow_neg, Field.zpow_neg, ofRat_inv]
-    congr 1
-    have : (1 : Int) = (1 : Nat) := rfl
-    rw [this, ← Int.natCast_add, Rat.zpow_natCast, Field.zpow_natCast, ofRat_npow' ha]
-
-theorem ofRat_zpow {α} [Field α] [IsCharP α 0] (a : Rat) (n : Int) : (ofRat (a^n) : α) = ofRat a ^ n := by
-  cases n
-  next => rw [Int.ofNat_eq_natCast, Rat.zpow_natCast, Field.zpow_natCast, ofRat_npow]
-  next =>
-    rw [Int.negSucc_eq, Rat.zpow_neg, Field.zpow_neg, ofRat_inv]
-    congr 1
-    have : (1 : Int) = (1 : Nat) := rfl
-    rw [this, ← Int.natCast_add, Rat.zpow_natCast, Field.zpow_natCast, ofRat_npow]
-
-theorem natCast_eq {α} [Field α] (n : Nat) : (NatCast.natCast n : α) = ofRat n := by
-  simp [ofRat, Ring.intCast_natCast, Semiring.natCast_one, Field.div_eq_mul_inv,
-        Field.inv_one, Semiring.mul_one]
-
-theorem ofNat_eq {α} [Field α] (n : Nat) : (OfNat.ofNat n : α) = ofRat n := by
-  rw [Semiring.ofNat_eq_natCast]
-  apply natCast_eq
-
-theorem intCast_eq {α} [Field α] (n : Int) : (IntCast.intCast n : α) = ofRat n := by
-  simp [ofRat, Semiring.natCast_one, Field.div_eq_mul_inv, Field.inv_one, Semiring.mul_one]
-
-theorem add_eq {α} [Field α] [IsCharP α 0] (a b : α) (v₁ v₂ v : Rat)
-    : v == v₁ + v₂ → a = ofRat v₁ → b = ofRat v₂ → a + b = ofRat v := by
-  simp; intros; subst v a b; rw [ofRat_add]
-
-theorem sub_eq {α} [Field α] [IsCharP α 0] (a b : α) (v₁ v₂ v : Rat)
-    : v == v₁ - v₂ → a = ofRat v₁ → b = ofRat v₂ → a - b = ofRat v := by
-  simp; intros; subst v a b; rw [ofRat_sub]
-
-theorem mul_eq {α} [Field α] [IsCharP α 0] (a b : α) (v₁ v₂ v : Rat)
-    : v == v₁ * v₂ → a = ofRat v₁ → b = ofRat v₂ → a * b = ofRat v := by
-  simp; intros; subst v a b; rw [ofRat_mul]
-
-theorem div_eq {α} [Field α] [IsCharP α 0] (a b : α) (v₁ v₂ v : Rat)
-    : v == v₁ / v₂ → a = ofRat v₁ → b = ofRat v₂ → a / b = ofRat v := by
-  simp; intros; subst v a b; rw [ofRat_div]
-
-theorem inv_eq {α} [Field α] (a : α) (v₁ v : Rat)
-    : v == v₁⁻¹ → a = ofRat v₁ → a⁻¹ = ofRat v := by
-  simp; intros; subst v a; rw [ofRat_inv]
-
-theorem neg_eq {α} [Field α] (a : α) (v₁ v : Rat)
-    : v == -v₁ → a = ofRat v₁ → -a = ofRat v := by
-  simp; intros; subst v a; rw [ofRat_neg]
-
-theorem npow_eq {α} [Field α] [IsCharP α 0] (a : α) (n : Nat) (v₁ v : Rat)
-    : v == v₁^n → a = ofRat v₁ → a ^ n = ofRat v := by
-  simp; intros; subst v a; rw [ofRat_npow]
-
-theorem zpow_eq {α} [Field α] [IsCharP α 0] (a : α) (n : Int) (v₁ v : Rat)
-    : v == v₁^n → a = ofRat v₁ → a ^ n = ofRat v := by
-  simp; intros; subst v a; rw [ofRat_zpow]
-
-theorem eq_int {α} [Field α] (a : α) (v : Rat) (n : Int)
-    : n == v.num && v.den == 1 → a = ofRat v → a = IntCast.intCast n := by
-  simp; cases v; simp [ofRat]
-  next den _ _ =>
-  intros; subst den n a
-  simp [Semiring.natCast_one, Field.div_eq_mul_inv, Field.inv_one, Semiring.mul_one]
-
-theorem eq_inv {α} [Field α] (a : α) (v : Rat) (d : Nat)
-    : v.num == 1 && v.den == d → a = ofRat v → a = (NatCast.natCast d : α)⁻¹ := by
-  simp; cases v; simp [ofRat]
-  next num _ _ _ =>
-  intros; subst num d a
-  simp [Ring.intCast_one, Field.div_eq_mul_inv, Semiring.one_mul]
-
-theorem eq_mul_inv {α} [Field α] (a : α) (v : Rat) (n : Int) (d : Nat)
-    : v.num == n && v.den == d → a = ofRat v → a = (IntCast.intCast n : α) * (NatCast.natCast d : α)⁻¹ := by
-  cases v; simp [ofRat]
-  intros; subst d n a
-  simp [Field.div_eq_mul_inv]
-
-end Lean.Grind.Field.NormNum

src/Init/Grind/Interactive.lean

@@ -72,9 +72,7 @@ syntax (name := linarith) "linarith" : grind
 /-- The `sorry` tactic is a temporary placeholder for an incomplete tactic proof. -/
 syntax (name := «sorry») "sorry" : grind
 
-syntax thmNs := &"namespace" ident
-
-syntax thm := anchor <|> thmNs <|> grindLemmaMin <|> grindLemma
+syntax thm := anchor <|> grindLemmaMin <|> grindLemma
 
 /--
 Instantiates theorems using E-matching.

src/Init/Grind/Ordered/Ring.lean

@@ -236,21 +236,20 @@ instance [Ring R] [LE R] [LT R] [LawfulOrderLT R] [IsPreorder R] [OrderedRing R]
 
 end Preorder
 
-theorem mul_pos [LE R] [LT R] [IsPreorder R] [OrderedRing R] {a b : R} (h₁ : 0 < a) (h₂ : 0 < b) : 0 < a * b := by
-  simpa [Semiring.zero_mul] using mul_lt_mul_of_pos_right h₁ h₂
-
-theorem zero_le_one [LE R] [LT R] [LawfulOrderLT R] [IsPreorder R] [OrderedRing R] : (0 : R) ≤ 1 :=
-  Preorder.le_of_lt zero_lt_one
-
-theorem not_one_lt_zero [LE R] [LT R] [LawfulOrderLT R] [IsPreorder R] [OrderedRing R] : ¬ ((1 : R) < 0) :=
-  fun h => Preorder.lt_irrefl (0 : R) (Preorder.lt_trans zero_lt_one h)
-
 section PartialOrder
 
 variable [LE R] [LT R] [IsPartialOrder R] [OrderedRing R]
 
+theorem mul_pos {a b : R} (h₁ : 0 < a) (h₂ : 0 < b) : 0 < a * b := by
+  simpa [Semiring.zero_mul] using mul_lt_mul_of_pos_right h₁ h₂
+
 variable [LawfulOrderLT R]
 
+theorem zero_le_one : (0 : R) ≤ 1 := Preorder.le_of_lt zero_lt_one
+
+theorem not_one_lt_zero : ¬ ((1 : R) < 0) :=
+  fun h => Preorder.lt_irrefl (0 : R) (Preorder.lt_trans zero_lt_one h)
+
 theorem mul_le_mul_of_nonneg_left {a b c : R} (h : a ≤ b) (h' : 0 ≤ c) : c * a ≤ c * b := by
   rw [PartialOrder.le_iff_lt_or_eq] at h'
   cases h' with

src/Init/Grind/Ring/Basic.lean

@@ -82,10 +82,6 @@ class Semiring (α : Type u) extends Add α, Mul α where
   ofNat_succ : ∀ a : Nat, OfNat.ofNat (α := α) (a + 1) = OfNat.ofNat a + 1 := by intros; rfl
   /-- Numerals are consistently defined with respect to the canonical map from natural numbers. -/
   ofNat_eq_natCast : ∀ n : Nat, OfNat.ofNat (α := α) n = Nat.cast n := by intros; rfl
-  /--
-  Multiplying by a numeral is consistently defined with respect to the canonical map from natural
-  numbers.
-  -/
   nsmul_eq_natCast_mul : ∀ n : Nat, ∀ a : α, n • a = Nat.cast n * a := by intros; rfl
 
 /--
@@ -208,11 +204,6 @@ theorem pow_add (a : α) (k₁ k₂ : Nat) : a ^ (k₁ + k₂) = a^k₁ * a^k₂
 theorem pow_add_congr (a r : α) (k k₁ k₂ : Nat) : k = k₁ + k₂ → a^k₁ * a^k₂ = r → a ^ k = r := by
   intros; subst k r; rw [pow_add]
 
-theorem one_pow (n : Nat) : (1 : α) ^ n = 1 := by
-  induction n
-  next => simp [pow_zero]
-  next => simp [pow_succ, *, mul_one]
-
 theorem natCast_pow (x : Nat) (k : Nat) : ((x ^ k : Nat) : α) = (x : α) ^ k := by
   induction k
   next => simp [pow_zero, Nat.pow_zero, natCast_one]
@@ -385,11 +376,6 @@ variable {α : Type u} [CommSemiring α]
 theorem mul_left_comm (a b c : α) : a * (b * c) = b * (a * c) := by
   rw [← mul_assoc, ← mul_assoc, mul_comm a]
 
-theorem mul_pow (a b : α) (n : Nat) : (a*b)^n = a^n * b^n := by
-  induction n
-  next => simp [pow_zero, mul_one]
-  next n ih => simp [pow_succ, ih, mul_comm, mul_assoc, mul_left_comm]
-
 end CommSemiring
 
 open Semiring hiding add_comm add_assoc add_zero

src/Init/Grind/Ring/CommSolver.lean

@@ -656,29 +656,6 @@ noncomputable def Expr.toPoly_k (e : Expr) : Poly :=
       (k.beq 0))
     e
 
-def Mon.degreeOf (m : Mon) (x : Var) : Nat :=
-  match m with
-  | .unit => 0
-  | .mult pw m => bif pw.x == x then pw.k else degreeOf m x
-
-def Mon.cancelVar (m : Mon) (x : Var) : Mon :=
-  match m with
-  | .unit => .unit
-  | .mult pw m => bif pw.x == x then m else .mult pw (cancelVar m x)
-
-def Poly.cancelVar' (c : Int) (x : Var) (p : Poly) (acc : Poly) : Poly :=
-  match p with
-  | .num k => acc.addConst k
-  | .add k m p =>
-    let n := m.degreeOf x
-    bif n > 0 && c^n ∣ k then
-      cancelVar' c x p (acc.insert (k / (c^n)) (m.cancelVar x))
-    else
-      cancelVar' c x p (acc.insert k m)
-
-def Poly.cancelVar (c : Int) (x : Var) (p : Poly) : Poly :=
-  cancelVar' c x p (.num 0)
-
 @[simp] theorem Expr.toPoly_k_eq_toPoly (e : Expr) : e.toPoly_k = e.toPoly := by
   induction e <;> simp only [toPoly, toPoly_k]
   next a ih => rw [Poly.mulConst_k_eq_mulConst]; congr
@@ -1198,72 +1175,6 @@ theorem Expr.eq_of_toPoly_nc_eq {α} [Ring α] (ctx : Context α) (a b : Expr) (
   simp [denote_toPoly_nc] at h
   assumption
 
-section
-attribute [local simp] Semiring.pow_zero Semiring.mul_one Semiring.one_mul cond_eq_ite
-
-theorem Mon.denote_cancelVar [CommSemiring α] (ctx : Context α) (m : Mon) (x : Var)
-    : m.denote ctx = x.denote ctx ^ (m.degreeOf x) * (m.cancelVar x).denote ctx := by
-  fun_induction cancelVar <;> simp [degreeOf]
-  next h =>
-    simp at h; simp [*, denote, Power.denote_eq]
-  next h ih =>
-    simp at h; simp [*, denote, Semiring.mul_assoc, CommSemiring.mul_comm, CommSemiring.mul_left_comm]
-
-theorem Poly.denote_cancelVar' {α} [CommRing α] (ctx : Context α) (p : Poly) (c : Int) (x : Var) (acc : Poly)
-    : c ≠ 0 → c * x.denote ctx = 1 → (p.cancelVar' c x acc).denote ctx = p.denote ctx + acc.denote ctx := by
-  intro h₁ h₂
-  fun_induction cancelVar'
-  next acc k => simp [denote_addConst, denote, Semiring.add_comm]
-  next h ih =>
-    simp [ih, denote_insert, denote]
-    conv => rhs; rw [Mon.denote_cancelVar (x := x)]
-    simp [← Semiring.add_assoc]
-    congr 1
-    rw [Semiring.add_comm, Ring.zsmul_eq_intCast_mul,]
-    congr 1
-    simp +zetaDelta [Int.dvd_def] at h
-    have ⟨d, h⟩ := h.2
-    simp +zetaDelta [h]
-    rw [Int.mul_ediv_cancel_left _ (Int.pow_ne_zero h₁)]
-    rw [Ring.intCast_mul]
-    conv => rhs; lhs; rw [CommSemiring.mul_comm]
-    rw [Semiring.mul_assoc, Ring.intCast_pow]
-    congr 1
-    rw [← Semiring.mul_assoc, ← CommSemiring.mul_pow, h₂, Semiring.one_pow, Semiring.one_mul]
-  next ih =>
-    simp [ih, denote_insert, denote, Ring.zsmul_eq_intCast_mul, Semiring.add_assoc,
-      Semiring.add_comm, add_left_comm]
-
-theorem Poly.denote_cancelVar {α} [CommRing α] (ctx : Context α) (p : Poly) (c : Int) (x : Var)
-    : c ≠ 0 → c * x.denote ctx = 1 → (p.cancelVar c x).denote ctx = p.denote ctx := by
-  intro h₁ h₂
-  have := denote_cancelVar' ctx p c x (.num 0) h₁ h₂
-  rw [cancelVar, this, denote, Ring.intCast_zero, Semiring.add_zero]
-
-noncomputable def cancel_var_cert (c : Int) (x : Var) (p₁ p₂ : Poly) : Bool :=
-  c != 0 && p₂.beq' (p₁.cancelVar c x)
-
-theorem eq_cancel_var {α} [CommRing α] (ctx : Context α) (c : Int) (x : Var) (p₁ p₂ : Poly)
-    : cancel_var_cert c x p₁ p₂ → c * x.denote ctx = 1 → p₁.denote ctx = 0 → p₂.denote ctx = 0 := by
-  simp [cancel_var_cert]; intros h₁ _ h₂ _; subst p₂
-  simp [Poly.denote_cancelVar ctx p₁ c x h₁ h₂]; assumption
-
-theorem diseq_cancel_var {α} [CommRing α] (ctx : Context α) (c : Int) (x : Var) (p₁ p₂ : Poly)
-    : cancel_var_cert c x p₁ p₂ → c * x.denote ctx = 1 → p₁.denote ctx ≠ 0 → p₂.denote ctx ≠ 0 := by
-  simp [cancel_var_cert]; intros h₁ _ h₂ _; subst p₂
-  simp [Poly.denote_cancelVar ctx p₁ c x h₁ h₂]; assumption
-
-theorem le_cancel_var {α} [CommRing α] [LE α] (ctx : Context α) (c : Int) (x : Var) (p₁ p₂ : Poly)
-    : cancel_var_cert c x p₁ p₂ → c * x.denote ctx = 1 → p₁.denote ctx ≤ 0 → p₂.denote ctx ≤ 0 := by
-  simp [cancel_var_cert]; intros h₁ _ h₂ _; subst p₂
-  simp [Poly.denote_cancelVar ctx p₁ c x h₁ h₂]; assumption
-
-theorem lt_cancel_var {α} [CommRing α] [LT α] (ctx : Context α) (c : Int) (x : Var) (p₁ p₂ : Poly)
-    : cancel_var_cert c x p₁ p₂ → c * x.denote ctx = 1 → p₁.denote ctx < 0 → p₂.denote ctx < 0 := by
-  simp [cancel_var_cert]; intros h₁ _ h₂ _; subst p₂
-  simp [Poly.denote_cancelVar ctx p₁ c x h₁ h₂]; assumption
-
-end
 /-!
 Theorems for justifying the procedure for commutative rings with a characteristic in `grind`.
 -/
@@ -1487,21 +1398,6 @@ theorem mul {α} [CommRing α] (ctx : Context α) (p₁ : Poly) (k : Int) (p : P
   simp [mul_cert]; intro _ h; subst p
   simp [Poly.denote_mulConst, *, mul_zero]
 
-theorem eq_mul {α} [CommRing α] (ctx : Context α) (p₁ : Poly) (k : Int) (p : Poly)
-    : mul_cert p₁ k p → p₁.denote ctx = 0 → p.denote ctx = 0 := by
-  apply mul
-
-noncomputable def mul_ne_cert (p₁ : Poly) (k : Int) (p : Poly) : Bool :=
-  k != 0 && (p₁.mulConst_k k |>.beq' p)
-
-theorem diseq_mul {α} [CommRing α] [NoNatZeroDivisors α] (ctx : Context α) (p₁ : Poly) (k : Int) (p : Poly)
-    : mul_ne_cert p₁ k p → p₁.denote ctx ≠ 0 → p.denote ctx ≠ 0 := by
-  simp [mul_ne_cert]; intro h₁ _ h₂; subst p
-  simp [Poly.denote_mulConst]; intro h₃
-  rw [← zsmul_eq_intCast_mul] at h₃
-  have := no_int_zero_divisors h₁ h₃
-  contradiction
-
 theorem inv {α} [CommRing α] (ctx : Context α) (p₁ : Poly) (p : Poly)
     : mul_cert p₁ (-1) p → p₁.denote ctx = 0 → p.denote ctx = 0 :=
   mul ctx p₁ (-1) p
@@ -1712,16 +1608,6 @@ theorem le_int_module {α} [CommRing α] [LE α] (ctx : Context α) (p : Poly)
     : p.denote ctx ≤ 0 → p.denoteAsIntModule ctx ≤ 0 := by
   simp [Poly.denoteAsIntModule_eq_denote]
 
-noncomputable def mul_ineq_cert (p₁ : Poly) (k : Int) (p : Poly) : Bool :=
-  k > 0 && (p₁.mulConst_k k |>.beq' p)
-
-theorem le_mul {α} [CommRing α] [LE α] [LT α] [IsPreorder α] [OrderedRing α] (ctx : Context α) (p₁ : Poly) (k : Int) (p : Poly)
-    : mul_ineq_cert p₁ k p → p₁.denote ctx ≤ 0 → p.denote ctx ≤ 0 := by
-  simp [mul_ineq_cert]; intro h₁ _ h₂; subst p; simp [Poly.denote_mulConst]
-  replace h₂ := zsmul_nonpos (Int.le_of_lt h₁) h₂
-  simp [Ring.zsmul_eq_intCast_mul] at h₂
-  assumption
-
 theorem lt_norm {α} [CommRing α] [LE α] [LT α] [LawfulOrderLT α] [IsPreorder α] [OrderedRing α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
     : core_cert lhs rhs p → lhs.denote ctx < rhs.denote ctx → p.denote ctx < 0 := by
   simp [core_cert]; intro _ h; subst p; simp [Expr.denote_toPoly, Expr.denote]
@@ -1733,13 +1619,6 @@ theorem lt_int_module {α} [CommRing α] [LT α] (ctx : Context α) (p : Poly)
     : p.denote ctx < 0 → p.denoteAsIntModule ctx < 0 := by
   simp [Poly.denoteAsIntModule_eq_denote]
 
-theorem lt_mul {α} [CommRing α] [LE α] [LT α] [LawfulOrderLT α] [IsPreorder α] [OrderedRing α] (ctx : Context α) (p₁ : Poly) (k : Int) (p : Poly)
-    : mul_ineq_cert p₁ k p → p₁.denote ctx < 0 → p.denote ctx < 0 := by
-  simp [mul_ineq_cert]; intro h₁ _ h₂; subst p; simp [Poly.denote_mulConst]
-  replace h₂ := zsmul_neg_iff k h₂ |>.mpr h₁
-  simp [Ring.zsmul_eq_intCast_mul] at h₂
-  assumption
-
 theorem not_le_norm {α} [CommRing α] [LE α] [LT α] [LawfulOrderLT α] [IsLinearOrder α] [OrderedRing α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
     : core_cert rhs lhs p → ¬ lhs.denote ctx ≤ rhs.denote ctx → p.denote ctx < 0 := by
   simp [core_cert]; intro _ h₁; subst p; simp [Expr.denote_toPoly, Expr.denote]
@@ -1763,13 +1642,6 @@ theorem inv_int_eq [Field α] [IsCharP α 0] (b : Int) : b != 0 → (denoteInt b
     have := IsCharP.intCast_eq_zero_iff (α := α) 0 b; simp [*] at this
   rw [Field.mul_inv_cancel this]
 
-theorem intCast_eq_denoteInt [Field α] (b : Int) : (IntCast.intCast b : α) = denoteInt b := by
-  simp [denoteInt_eq]
-
-theorem inv_int_eq' [Field α] [IsCharP α 0] (b : Int) : b != 0 → (IntCast.intCast b : α) * (denoteInt b)⁻¹ = 1 := by
-  rw [intCast_eq_denoteInt]
-  apply inv_int_eq
-
 theorem inv_int_eqC {α c} [Field α] [IsCharP α c] (b : Int) : b % c != 0 → (denoteInt b : α) * (denoteInt b)⁻¹ = 1 := by
   simp; intro h
   have : (denoteInt b : α) ≠ 0 := by

src/Init/Grind/Ring/Field.lean

@@ -16,7 +16,6 @@ namespace Lean.Grind
 A field is a commutative ring with inverses for all non-zero elements.
 -/
 class Field (α : Type u) extends CommRing α, Inv α, Div α where
-  /-- An exponentiation operator. -/
   [zpow : HPow α Int α]
   /-- Division is multiplication by the inverse. -/
   div_eq_mul_inv : ∀ a b : α, a / b = a * b⁻¹
@@ -95,7 +94,7 @@ theorem inv_eq_zero_iff {a : α} : a⁻¹ = 0 ↔ a = 0 := by
 theorem zero_eq_inv_iff {a : α} : 0 = a⁻¹ ↔ 0 = a := by
   rw [eq_comm, inv_eq_zero_iff, eq_comm]
 
-theorem of_mul_eq_zero {a b : α} : a * b = 0 → a = 0 ∨ b = 0 := by
+theorem of_mul_eq_zero {a b : α} : a*b = 0 → a = 0 ∨ b = 0 := by
   cases (Classical.em (a = 0)); · simp [*, Semiring.zero_mul]
   cases (Classical.em (b = 0)); · simp [*, Semiring.mul_zero]
   rename_i h₁ h₂
@@ -170,52 +169,6 @@ theorem zpow_add {a : α} (h : a ≠ 0) (m n : Int) : a ^ (m + n) = a ^ m * a ^
     | zero => simp [Int.add_neg_one, zpow_sub_one h, zpow_neg_one]
     | succ n ih => rw [Int.natCast_add_one, Int.neg_add, Int.add_neg_one, ← Int.add_sub_assoc, zpow_sub_one h, zpow_sub_one h, ih, Semiring.mul_assoc]
 
-theorem div_zero {x : α} : x / 0 = 0 := by rw [div_eq_mul_inv, inv_zero, Semiring.mul_zero]
-
-theorem mul_div {x y z : α} : x * (y / z) = (x * y) / z := by
-  rw [div_eq_mul_inv, div_eq_mul_inv, Semiring.mul_assoc]
-theorem div_mul {x y z : α} : x / y * z = x * z / y := by
-  rw [div_eq_mul_inv, div_eq_mul_inv, Semiring.mul_assoc, CommSemiring.mul_comm y⁻¹,
-    Semiring.mul_assoc]
-theorem div_add {x y z : α} (hy : y ≠ 0) : x / y + z = (x + y * z) / y := by
-  rw [div_eq_mul_inv, div_eq_mul_inv, Semiring.right_distrib, CommSemiring.mul_comm y,
-    Semiring.mul_assoc, Field.mul_inv_cancel hy, Semiring.mul_one]
-theorem add_div {x y z : α} (hz : z ≠ 0) : x + y / z = (x * z + y) / z := by
-  rw [div_eq_mul_inv, div_eq_mul_inv, Semiring.right_distrib, Semiring.mul_assoc,
-    Field.mul_inv_cancel hz, Semiring.mul_one]
-
-theorem div_div_right {x y z : α} : x / (y / z) = x * z / y := by
-  rw [div_eq_mul_inv, div_eq_mul_inv, div_eq_mul_inv, inv_mul, inv_inv, CommSemiring.mul_comm y⁻¹,
-    Semiring.mul_assoc]
-theorem div_div_left {x y z : α} : (x / y) / z = x / (y * z) := by
-  rw [div_eq_mul_inv, div_eq_mul_inv, div_eq_mul_inv, inv_mul, Semiring.mul_assoc]
-theorem div_mul_cancel {x y : α} (h : y ≠ 0) : x / y * y = x := by
-  rw [div_eq_mul_inv, Semiring.mul_assoc, Field.inv_mul_cancel h, Semiring.mul_one]
-
-attribute [local instance] Semiring.natCast in
-theorem natCast_ne_zero [IsCharP α 0] {n : Nat} (h : n ≠ 0) : (n : α) ≠ 0 := by
-    simpa [IsCharP.natCast_eq_zero_iff]
-
-attribute [local instance] Ring.intCast in
-theorem intCast_div_of_dvd {x y : Int} (h : y ∣ x) (w : (y : α) ≠ 0) :
-    ((x / y : Int) : α) = ((x : α) / (y : α)) := by
-  obtain ⟨z, rfl⟩ := h
-  by_cases hy : y = 0
-  · simp_all [Ring.intCast_zero]
-  · rw [Int.mul_ediv_cancel_left _ hy]
-    rw [Ring.intCast_mul, CommSemiring.mul_comm, div_eq_mul_inv, Semiring.mul_assoc,
-      mul_inv_cancel w, Semiring.mul_one]
-
-attribute [local instance] Semiring.natCast in
-theorem natCast_div_of_dvd {x y : Nat} (h : y ∣ x) (w : (y : α) ≠ 0) :
-    ((x / y : Nat) : α) = ((x : α) / (y : α)) := by
-  obtain ⟨z, rfl⟩ := h
-  by_cases hy : y = 0
-  · simp_all [Semiring.natCast_zero]
-  · rw [Nat.mul_div_cancel_left _ (by omega)]
-    rw [Semiring.natCast_mul, CommSemiring.mul_comm, div_eq_mul_inv, Semiring.mul_assoc,
-      mul_inv_cancel w, Semiring.mul_one]
-
 -- This is expensive as an instance. Let's see what breaks without it.
 def noNatZeroDivisors.ofIsCharPZero [IsCharP α 0] : NoNatZeroDivisors α := NoNatZeroDivisors.mk' <| by
   intro a b h w

src/Init/Prelude.lean

@@ -3449,11 +3449,11 @@ structure String where ofByteArray ::
   /-- The bytes of the UTF-8 encoding of the string. Since strings have a special representation in
   the runtime, this function actually takes linear time and space at runtime. For efficient access
   to the string's bytes, use `String.utf8ByteSize` and `String.getUTF8Byte`. -/
-  toByteArray : ByteArray
+  bytes : ByteArray
   /-- The bytes of the string form valid UTF-8. -/
-  isValidUTF8 : ByteArray.IsValidUTF8 toByteArray
+  isValidUTF8 : ByteArray.IsValidUTF8 bytes
 
-attribute [extern "lean_string_to_utf8"] String.toByteArray
+attribute [extern "lean_string_to_utf8"] String.bytes
 attribute [extern "lean_string_from_utf8_unchecked"] String.ofByteArray
 
 /--
@@ -3468,7 +3468,7 @@ def String.decEq (s₁ s₂ : @& String) : Decidable (Eq s₁ s₂) :=
   | ⟨⟨⟨s₁⟩⟩, _⟩, ⟨⟨⟨s₂⟩⟩, _⟩ =>
     dite (Eq s₁ s₂) (fun h => match s₁, s₂, h with | _, _, Eq.refl _ => isTrue rfl)
       (fun h => isFalse
-        (fun h' => h (congrArg (fun s => Array.toList (ByteArray.data (String.toByteArray s))) h')))
+        (fun h' => h (congrArg (fun s => Array.toList (ByteArray.data (String.bytes s))) h')))
 
 instance : DecidableEq String := String.decEq
 
@@ -3482,7 +3482,7 @@ be translated internally to byte positions, which takes linear time.
 A byte position `p` is *valid* for a string `s` if `0 ≤ p ≤ s.rawEndPos` and `p` lies on a UTF-8
 character boundary, see `String.Pos.IsValid`.
 
-There is another type, `String.Pos`, which bundles the validity predicate. Using `String.Pos`
+There is another type, `String.ValidPos`, which bundles the validity predicate. Using `String.ValidPos`
 instead of `String.Pos.Raw` is recommended because it will lead to less error handling and fewer edge cases.
 -/
 structure String.Pos.Raw where
@@ -3534,7 +3534,7 @@ At runtime, this function takes constant time because the byte length of strings
 -/
 @[extern "lean_string_utf8_byte_size"]
 def String.utf8ByteSize (s : @& String) : Nat :=
-  s.toByteArray.size
+  s.bytes.size
 
 /--
 A UTF-8 byte position that points at the end of a string, just after the last character.

src/Init/System/FilePath.lean

@@ -93,7 +93,7 @@ An absolute path starts at the root directory or a drive letter. Accessing files
 path does not depend on the current working directory.
 -/
 def isAbsolute (p : FilePath) : Bool :=
-  pathSeparators.contains p.toString.front || (isWindows && p.toString.length > 1 && p.toString.startPos.next?.bind (·.get?) == some ':')
+  pathSeparators.contains p.toString.front || (isWindows && p.toString.length > 1 && p.toString.startValidPos.next?.bind (·.get?) == some ':')
 
 /--
 A relative path is one that depends on the current working directory for interpretation. Relative
@@ -122,7 +122,7 @@ instance : HDiv FilePath String FilePath where
   hDiv p sub := FilePath.join p ⟨sub⟩
 
 private def posOfLastSep (p : FilePath) : Option String.Pos.Raw :=
-  p.toString.revFind? pathSeparators.contains |>.map String.Pos.offset
+  p.toString.revFind? pathSeparators.contains |>.map String.ValidPos.offset
 
 /--
 Returns the parent directory of a path, if there is one.
@@ -173,7 +173,7 @@ Examples:
 -/
 def fileStem (p : FilePath) : Option String :=
   p.fileName.map fun fname =>
-    match fname.revFind? '.' |>.map String.Pos.offset with
+    match fname.revFind? '.' |>.map String.ValidPos.offset with
     | some ⟨0⟩ => fname
     | some pos => String.Pos.Raw.extract fname 0 pos
     | none     => fname
@@ -192,7 +192,7 @@ Examples:
 -/
 def extension (p : FilePath) : Option String :=
   p.fileName.bind fun fname =>
-    match fname.revFind? '.' |>.map String.Pos.offset with
+    match fname.revFind? '.' |>.map String.ValidPos.offset with
     | some 0   => none
     | some pos => some <| String.Pos.Raw.extract fname (pos + '.') fname.rawEndPos
     | none     => none

src/Init/System/IO.lean

@@ -565,20 +565,9 @@ Waits until any of the tasks in the list has finished, then return its result.
     (h : tasks.length > 0 := by exact Nat.zero_lt_succ _) : BaseIO α :=
   return tasks[0].get
 
-/--
-Given a non-empty list of tasks, wait for the first to complete.
-Return the value and the list of remaining tasks.
--/
-def waitAny' (tasks : List (Task α)) (h : 0 < tasks.length := by exact Nat.zero_lt_succ _) :
-    BaseIO (α × List (Task α)) := do
-  let (i, a) ← IO.waitAny
-    (tasks.mapIdx fun i t => t.map (sync := true) fun a => (i, a))
-    (by simp_all)
-  return (a, tasks.eraseIdx i)
-
 /--
 Returns the number of _heartbeats_ that have occurred during the current thread's execution. The
-heartbeat count is the number of "small" memory allocations performed in a thread.
+heartbeat count is the number of “small” memory allocations performed in a thread.
 
 Heartbeats used to implement timeouts that are more deterministic across different hardware.
 -/

src/Init/Try.lean

@@ -55,9 +55,6 @@ syntax (name := tryTrace) "try?" optConfig : tactic
 /-- Helper internal tactic for implementing the tactic `try?`. -/
 syntax (name := attemptAll) "attempt_all " withPosition((ppDedent(ppLine) colGe "| " tacticSeq)+) : tactic
 
-/-- Helper internal tactic for implementing the tactic `try?` with parallel execution. -/
-syntax (name := attemptAllPar) "attempt_all_par " withPosition((ppDedent(ppLine) colGe "| " tacticSeq)+) : tactic
-
 /-- Helper internal tactic used to implement `evalSuggest` in `try?` -/
 syntax (name := tryResult) "try_suggestions " tactic* : tactic
 

src/Init/While.lean

@@ -29,7 +29,7 @@ partial def Loop.forIn {β : Type u} {m : Type u → Type v} [Monad m] (_ : Loop
       | ForInStep.yield b => loop b
   loop init
 
-instance [Monad m] : ForIn m Loop Unit where
+instance : ForIn m Loop Unit where
   forIn := Loop.forIn
 
 syntax "repeat " doSeq : doElem

src/Lean/Compiler/ExternAttr.lean

@@ -76,7 +76,7 @@ builtin_initialize externAttr : ParametricAttribute ExternAttrData ←
 def getExternAttrData? (env : Environment) (n : Name) : Option ExternAttrData :=
   externAttr.getParam? env n
 
-private def parseOptNum : Nat → (pattern : String) → (it : pattern.Pos) → Nat → pattern.Pos × Nat
+private def parseOptNum : Nat → (pattern : String) → (it : pattern.ValidPos) → Nat → pattern.ValidPos × Nat
   | 0,   _      , it, r => (it, r)
   | n+1, pattern, it, r =>
     if h : it.IsAtEnd then (it, r)
@@ -86,7 +86,7 @@ private def parseOptNum : Nat → (pattern : String) → (it : pattern.Pos) →
       then parseOptNum n pattern (it.next h) (r*10 + (c.toNat - '0'.toNat))
       else (it, r)
 
-def expandExternPatternAux (args : List String) : Nat → (pattern : String) → (it : pattern.Pos) → String → String
+def expandExternPatternAux (args : List String) : Nat → (pattern : String) → (it : pattern.ValidPos) → String → String
   | 0,   _,       _,  r => r
   | i+1, pattern, it, r =>
     if h : it.IsAtEnd then r
@@ -99,7 +99,7 @@ def expandExternPatternAux (args : List String) : Nat → (pattern : String) →
         expandExternPatternAux args i pattern it (r ++ args.getD j "")
 
 def expandExternPattern (pattern : String) (args : List String) : String :=
-  expandExternPatternAux args pattern.length pattern pattern.startPos ""
+  expandExternPatternAux args pattern.length pattern pattern.startValidPos ""
 
 def mkSimpleFnCall (fn : String) (args : List String) : String :=
   fn ++ "(" ++ ((args.intersperse ", ").foldl (·++·) "") ++ ")"

src/Lean/Compiler/IR.lean

@@ -27,7 +27,6 @@ public import Lean.Compiler.IR.Sorry
 public import Lean.Compiler.IR.ToIR
 public import Lean.Compiler.IR.ToIRType
 public import Lean.Compiler.IR.Meta
-public import Lean.Compiler.IR.Toposort
 
 -- The following imports are not required by the compiler. They are here to ensure that there
 -- are no orphaned modules.
@@ -72,7 +71,6 @@ def compile (decls : Array Decl) : CompilerM (Array Decl) := do
   decls ← updateSorryDep decls
   logDecls `result decls
   checkDecls decls
-  decls ← toposortDecls decls
   addDecls decls
   inferMeta decls
   return decls

src/Lean/Compiler/IR/AddExtern.lean

@@ -8,7 +8,6 @@ module
 
 prelude
 public import Lean.Compiler.IR.Boxing
-import Lean.Compiler.IR.RC
 
 public section
 
@@ -27,12 +26,11 @@ def addExtern (declName : Name) (externAttrData : ExternAttrData) : CoreM Unit :
     type := b
     nextVarIndex := nextVarIndex + 1
   let irType ← toIRType type
-  let decls := #[.extern declName params irType externAttrData]
-  if !isPrivateName declName then
-    modifyEnv (Compiler.LCNF.setDeclPublic · declName)
-  let decls := ExplicitBoxing.addBoxedVersions (← Lean.getEnv) decls
-  let decls ← explicitRC decls
-  logDecls `result decls
-  addDecls decls
+  let decl := .extern declName params irType externAttrData
+  addDecl decl
+  if !isPrivateName decl.name then
+    modifyEnv (Compiler.LCNF.setDeclPublic · decl.name)
+  if ExplicitBoxing.requiresBoxedVersion (← Lean.getEnv) decl then
+    addDecl (ExplicitBoxing.mkBoxedVersion decl)
 
 end Lean.IR

src/Lean/Compiler/IR/Boxing.lean

@@ -26,6 +26,12 @@ Assumptions:
   `Expr.isShared`, `Expr.isTaggedPtr`, and `FnBody.set`.
 -/
 
+def mkBoxedName (n : Name) : Name :=
+  Name.mkStr n "_boxed"
+
+def isBoxedName (name : Name) : Bool :=
+  name matches .str _ "_boxed"
+
 abbrev N := StateM Nat
 
 private def N.mkFresh : N VarId :=

src/Lean/Compiler/IR/CompilerM.lean

@@ -139,20 +139,10 @@ def findEnvDecl (env : Environment) (declName : Name) (includeServer := false):
 private def findInterpDecl (env : Environment) (declName : Name) : Option Decl :=
   findEnvDecl (includeServer := true) env declName
 
-namespace ExplicitBoxing
-
-def mkBoxedName (n : Name) : Name :=
-  Name.mkStr n "_boxed"
-
-def isBoxedName (name : Name) : Bool :=
-  name matches .str _ "_boxed"
-
-end ExplicitBoxing
-
 /-- Like ``findInterpDecl env (declName ++ `_boxed)`` but with optimized negative lookup. -/
 @[export lean_ir_find_env_decl_boxed]
 private def findInterpDeclBoxed (env : Environment) (declName : Name) : Option Decl :=
-  let boxed := ExplicitBoxing.mkBoxedName declName
+  let boxed := declName ++ `_boxed
   -- Important: get module index of base name, not boxed version. Usually the interpreter never
   -- does negative lookups except in the case of `call_boxed` which must check whether a boxed
   -- version exists. If `declName` exists as an imported declaration but `declName'` doesn't, the

src/Lean/Compiler/IR/Toposort.lean

@@ -1,70 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Henrik Böving
--/
-module
-
-prelude
-public import Lean.Compiler.IR.CompilerM
-
-/-!
-This module "topologically sorts" an SCC of decls (an SCC of decls in the pipeline may in fact
-contain more than one SCC at the moment). This is relevant because EmitC relies on the invariant
-that the constants (and in particular also the closed terms) occur in a reverse topologically sorted
-order for emitting them.
--/
-
-namespace Lean.IR
-
-structure TopoState where
-  declsMap : Std.HashMap Name Decl
-  seen : Std.HashSet Name
-  order : Array Decl
-
-abbrev ToposortM := StateRefT TopoState CompilerM
-
-partial def toposort (decls : Array Decl) : CompilerM (Array Decl) := do
-  let declsMap := .ofList (decls.toList.map (fun d => (d.name, d)))
-  let (_, s) ← go decls |>.run {
-    declsMap,
-    seen := .emptyWithCapacity decls.size,
-    order := .emptyWithCapacity decls.size
-  }
-  return s.order
-where
-  go (decls : Array Decl) : ToposortM Unit := do
-    decls.forM process
-
-  process (decl : Decl) : ToposortM Unit := do
-    if (← get).seen.contains decl.name then
-      return ()
-
-    modify fun s => { s with seen := s.seen.insert decl.name }
-    let .fdecl (body := body) .. := decl | unreachable!
-    processBody body
-    modify fun s => { s with order := s.order.push decl }
-
-  processBody (b : FnBody) : ToposortM Unit := do
-    match b with
-    | .vdecl _ _ e b =>
-      match e with
-      | .fap c .. | .pap c .. =>
-        if let some decl := (← get).declsMap[c]? then
-          process decl
-      | _ => pure ()
-      processBody b
-    | .jdecl _ _ v b =>
-      processBody v
-      processBody b
-    | .case _ _ _ cs => cs.forM (fun alt => processBody alt.body)
-    | .jmp .. | .ret .. | .unreachable => return ()
-    | _ => processBody b.body
-
-
-public def toposortDecls (decls : Array Decl) : CompilerM (Array Decl) := do
-  let (externDecls, otherDecls) := decls.partition (fun decl => decl.isExtern)
-  let otherDecls ← toposort otherDecls
-  return externDecls ++ otherDecls
-
-end Lean.IR

src/Lean/Compiler/LCNF/ElimDeadBranches.lean

@@ -35,7 +35,7 @@ inductive Value where
   A set of values are possible.
   -/
   | choice (vs : List Value)
-  deriving Inhabited
+  deriving Inhabited, Repr
 
 namespace Value
 
@@ -43,36 +43,17 @@ namespace Value
 def maxValueDepth := 8
 
 protected partial def beq : Value → Value → Bool
-  | bot, bot => true
-  | top, top => true
-  | ctor i1 vs1 , ctor i2 vs2 =>
-    i1 == i2 && Array.isEqv vs1 vs2 Value.beq
-  | choice vs1 , choice vs2 =>
-    let isSubset as bs := as.all (fun a => bs.any fun b => Value.beq a b)
-    isSubset vs1 vs2 && isSubset vs2 vs1
-  | _, _ => false
+| bot, bot => true
+| top, top => true
+| ctor i1 vs1 , ctor i2 vs2 =>
+  i1 == i2 && Array.isEqv vs1 vs2 Value.beq
+| choice vs1 , choice vs2 =>
+  let isSubset as bs := as.all (fun a => bs.any fun b => Value.beq a b)
+  isSubset vs1 vs2 && isSubset vs2 vs1
+| _, _ => false
 
 instance : BEq Value := ⟨Value.beq⟩
 
-protected partial def toFormat : Value → Format
-  | bot => "⊥"
-  | top => "⊤"
-  | ctor i vs =>
-    if vs.isEmpty then
-      format i
-    else
-      .paren <| format i ++ .join (vs.toList.map fun v => " " ++ Value.toFormat v)
-  | choice vs =>
-    .paren <| .joinSep (vs.map Value.toFormat) " | "
-
-instance : Repr Value where
-  reprPrec v _ := Value.toFormat v
-
-def inductValOfCtor (ctorName : Name) (env : Environment) : InductiveVal := Id.run do
-  let some (.ctorInfo info) ← env.find? ctorName | unreachable!
-  let some (.inductInfo info) ← env.find? info.induct | unreachable!
-  return info
-
 mutual
 
 /--
@@ -81,60 +62,32 @@ is a constructor that is already contained within `vs` try to detect
 the difference between these values and merge them accordingly into a
 choice node further down the tree.
 -/
-partial def addChoice (env : Environment) (vs : List Value) (v : Value) : List Value :=
+partial def addChoice (vs : List Value) (v : Value) : List Value :=
   match vs, v with
   | [], v => [v]
-  | v1@(ctor i1 vs1) :: cs, ctor i2 vs2 =>
+  | v1@(ctor i1 _ ) :: cs, ctor i2 _ =>
     if i1 == i2 then
-      ctor i1 (Array.zipWith (merge env) vs1 vs2) :: cs
+      (merge v1 v) :: cs
     else
-      v1 :: addChoice env cs v
-  | _, _ => panic! s!"invalid addChoice {repr v} into {repr vs}"
+      v1 :: addChoice cs v
+  | _, _ => panic! "invalid addChoice"
 
 /--
 Merge two values into one. `bot` is the neutral element, `top` the annihilator.
 -/
-partial def merge (env : Environment) (v1 v2 : Value) : Value :=
-  let newValue :=
-    match v1, v2 with
-    | bot, v | v, bot => v
-    | top, _ | _, top => top
-    | ctor i1 vs1, ctor i2 vs2 =>
-      if i1 == i2 then
-        ctor i1 (Array.zipWith (merge env) vs1 vs2)
-      else
-        choice [v1, v2]
-    | choice vs1, choice vs2 =>
-      choice (vs1.foldl (addChoice env) vs2)
-    | choice vs, v | v, choice vs =>
-      choice (addChoice env vs v)
-  match newValue with
-  | .top | .bot => newValue
-  | .choice vs => cleanup vs
-  | .ctor ctorName .. =>
-    if eligible newValue && inductHasNumCtors ctorName env 1 then
-      top
+partial def merge (v1 v2 : Value) : Value :=
+  match v1, v2 with
+  | bot, v | v, bot => v
+  | top, _ | _, top => top
+  | ctor i1 vs1, ctor i2 vs2 =>
+    if i1 == i2 then
+      ctor i1 (Array.zipWith merge vs1 vs2)
     else
-      newValue
-where
-  cleanup (vs : List Value) : Value := Id.run do
-    if vs.all eligible then
-      let .ctor ctorName .. := vs.head! | unreachable!
-      if inductHasNumCtors ctorName env vs.length then
-        top
-      else
-        choice vs
-    else
-      choice vs
-
-  inductHasNumCtors (ctorName : Name) (env : Environment) (n : Nat) : Bool := Id.run do
-    let induct := inductValOfCtor ctorName env
-    n == induct.numCtors
-
-  @[inline]
-  eligible (value : Value) : Bool := Id.run do
-    let .ctor _ args := value | return false
-    args.all (· == .top)
+      choice [v1, v2]
+  | choice vs1, choice vs2 =>
+    choice (vs1.foldl addChoice vs2)
+  | choice vs, v | v, choice vs =>
+    choice (addChoice vs v)
 
 end
 
@@ -153,16 +106,19 @@ where
     | remainingDepth + 1 =>
       match v with
       | ctor i vs =>
-        let induct := inductValOfCtor i env
-        if forbiddenTypes.contains induct.name then
+        let typeName := i.getPrefix
+        if forbiddenTypes.contains typeName then
           top
         else
           let cont forbiddenTypes' :=
             ctor i (vs.map (go · forbiddenTypes' remainingDepth))
-          if induct.isRec then
-            cont <| forbiddenTypes.insert induct.name
-          else
-            cont forbiddenTypes
+          match env.find? typeName with
+          | some (.inductInfo type) =>
+            if type.isRec then
+              cont <| forbiddenTypes.insert typeName
+            else
+              cont forbiddenTypes
+          | _ => cont forbiddenTypes
       | choice vs =>
         let vs := vs.map (go · forbiddenTypes remainingDepth)
         if vs.elem top then
@@ -173,7 +129,7 @@ where
 
 /-- Widening operator that guarantees termination in our abstract interpreter. -/
 def widening (env : Environment) (v1 v2 : Value) : Value :=
-  truncate env (merge env v1 v2)
+  truncate env (merge v1 v2)
 
 /--
 Check whether a certain constructor is part of a `Value` by name.
@@ -581,9 +537,7 @@ def inferStep : InterpM Bool := do
     withReader (fun ctx => { ctx with currFnIdx := idx }) do
       decl.params.forM fun p => updateVarAssignment p.fvarId .top
       match decl.value with
-      | .code code .. =>
-        withTraceNode `Compiler.elimDeadBranches (fun _ => return m!"Analyzing {decl.name}") do
-          interpCode code
+      | .code code .. => interpCode code
       | .extern .. => updateCurrFnSummary .top
     let newVal ← getFunVal idx
     if currentVal != newVal then
@@ -593,14 +547,13 @@ def inferStep : InterpM Bool := do
 /--
 Run `inferStep` until it reaches a fix point.
 -/
-partial def inferMain (n : Nat := 0) : InterpM Unit := do
+partial def inferMain : InterpM Unit := do
   let ctx ← read
   modify fun s => { s with assignments := ctx.decls.map fun _ => {} }
   let modified ← inferStep
   if modified then
-    inferMain (n + 1)
+    inferMain
   else
-    trace[Compiler.elimDeadBranches] m!"Termination after {n} steps"
     return ()
 
 /--
@@ -650,11 +603,6 @@ end UnreachableBranches
 
 open UnreachableBranches in
 def Decl.elimDeadBranches (decls : Array Decl) : CompilerM (Array Decl) := do
-  /-
-  We sort declarations by size here to ensure that when we restart in inferStep it will mostly be
-  small declarations that get re-analyzed.
-  -/
-  let decls := decls.qsort (fun l r => (l.size, l.name.toString).lexLt (r.size, r.name.toString))
   let mut assignments := decls.map fun _ => {}
   let initialVal i :=
     /-
@@ -667,9 +615,7 @@ def Decl.elimDeadBranches (decls : Array Decl) : CompilerM (Array Decl) := do
   let mut funVals := decls.size.fold (init := .empty) fun i _ p => p.push (initialVal i)
   let ctx := { decls }
   let mut state := { assignments, funVals }
-  (_, state) ←
-    withTraceNode `Compiler.elimDeadBranches (fun _ => return m!"Analyzing block: {decls.map (·.name)}")
-      inferMain |>.run ctx |>.run state
+  (_, state) ← inferMain |>.run ctx |>.run state
   funVals := state.funVals
   assignments := state.assignments
   modifyEnv fun e =>

src/Lean/Compiler/LCNF/Specialize.lean

@@ -238,13 +238,7 @@ def mkKey (params : Array Param) (decls : Array CodeDecl) (body : LetValue) : Co
   let key := ToExpr.run do
     ToExpr.withParams params do
       ToExpr.mkLambdaM params (← ToExpr.abstractM body)
-  let pre e := do
-    -- beta reduce if possible
-    if e.isHeadBetaTarget then
-      return .visit e.headBeta
-    else
-      return .continue
-  let key ← Meta.MetaM.run' <| Meta.transform (usedLetOnly := true) key pre
+  let key ← Meta.MetaM.run' <| Meta.transform (usedLetOnly := true) key
   return normLevelParams key
 
 open Internalize in

src/Lean/Compiler/LCNF/StructProjCases.lean

@@ -19,10 +19,9 @@ def findStructCtorInfo? (typeName : Name) : CoreM (Option ConstructorVal) := do
   let some (.ctorInfo ctorInfo) := (← getEnv).find? ctorName | return none
   return ctorInfo
 
-def mkFieldParamsForCtorType (ctorType : Expr) (numParams : Nat) (numFields : Nat) :
-    CompilerM (Array Param) := do
-  let mut type ← Meta.MetaM.run' <| toLCNFType ctorType
-  type ← toMonoType type
+def mkFieldParamsForCtorType (ctorType : Expr) (numParams : Nat) (numFields : Nat)
+    : CompilerM (Array Param) := do
+  let mut type := ctorType
   for _ in *...numParams do
     match type with
     | .forallE _ _ body _ =>
@@ -32,7 +31,7 @@ def mkFieldParamsForCtorType (ctorType : Expr) (numParams : Nat) (numFields : Na
   for _ in *...numFields do
     match type with
     | .forallE name fieldType body _ =>
-      let param ← mkParam name fieldType false
+      let param ← mkParam name (← toMonoType fieldType) false
       fields := fields.push param
       type := body
     | _ => unreachable!

src/Lean/Compiler/NameMangling.lean

@@ -29,8 +29,8 @@ where finally
   simp [i, UInt32.lt_iff_toNat_lt, this]; omega
 
 
-def mangleAux (s : String) (pos : s.Pos) (r : String) : String :=
-  if h : pos = s.endPos then r else
+def mangleAux (s : String) (pos : s.ValidPos) (r : String) : String :=
+  if h : pos = s.endValidPos then r else
   let c := pos.get h
   let pos := pos.next h
   if c.isAlpha || c.isDigit then
@@ -46,16 +46,16 @@ def mangleAux (s : String) (pos : s.Pos) (r : String) : String :=
 termination_by pos
 
 public def mangle (s : String) : String :=
-  mangleAux s s.startPos ""
+  mangleAux s s.startValidPos ""
 
 end String
 
 namespace Lean
 
-def checkLowerHex : Nat → (s : String) → s.Pos → Bool
+def checkLowerHex : Nat → (s : String) → s.ValidPos → Bool
   | 0, _, _ => true
   | k + 1, s, pos =>
-    if h : pos = s.endPos then
+    if h : pos = s.endValidPos then
       false
     else
       let ch := pos.get h
@@ -69,19 +69,19 @@ def fromHex? (c : Char) : Option Nat :=
     some (c.val - 87).toNat
   else none
 
-def parseLowerHex? (k : Nat) (s : String) (p : s.Pos) (acc : Nat) :
-    Option (s.Pos × Nat) :=
+def parseLowerHex? (k : Nat) (s : String) (p : s.ValidPos) (acc : Nat) :
+    Option (s.ValidPos × Nat) :=
   match k with
   | 0 => some (p, acc)
   | k + 1 =>
-    if h : p = s.endPos then
+    if h : p = s.endValidPos then
       none
     else
       match fromHex? (p.get h) with
       | some d => parseLowerHex? k s (p.next h) (acc <<< 4 ||| d)
       | none => none
 
-theorem lt_of_parseLowerHex?_eq_some {k : Nat} {s : String} {p q : s.Pos} {acc : Nat}
+theorem lt_of_parseLowerHex?_eq_some {k : Nat} {s : String} {p q : s.ValidPos} {acc : Nat}
     {r : Nat} (hk : 0 < k) : parseLowerHex? k s p acc = some (q, r) → p < q := by
   fun_induction parseLowerHex? with
   | case1 => simp at hk
@@ -89,10 +89,10 @@ theorem lt_of_parseLowerHex?_eq_some {k : Nat} {s : String} {p q : s.Pos} {acc :
   | case3 p acc k h d x ih =>
     match k with
     | 0 => simpa [parseLowerHex?] using fun h _ => h ▸ p.lt_next
-    | k + 1 => exact fun h => String.Pos.lt_trans p.lt_next (ih (by simp) h)
+    | k + 1 => exact fun h => String.ValidPos.lt_trans p.lt_next (ih (by simp) h)
   | case4 => simp
 
-def checkDisambiguation (s : String) (p : s.Pos) : Bool :=
+def checkDisambiguation (s : String) (p : s.ValidPos) : Bool :=
   if h : _ then
     let b := p.get h
     if b = '_' then
@@ -111,8 +111,8 @@ termination_by p
 
 def needDisambiguation (prev : Name) (next : String) : Bool :=
   (match prev with
-    | .str _ s => ∃ h, (s.endPos.prev h).get (by simp) = '_'
-    | _ => false) || checkDisambiguation next next.startPos
+    | .str _ s => ∃ h, (s.endValidPos.prev h).get (by simp) = '_'
+    | _ => false) || checkDisambiguation next next.startValidPos
 
 def Name.mangleAux : Name → String
   | Name.anonymous => ""
@@ -120,7 +120,7 @@ def Name.mangleAux : Name → String
     let m := String.mangle s
     match p with
     | Name.anonymous =>
-      if checkDisambiguation m m.startPos then "00" ++ m else m
+      if checkDisambiguation m m.startValidPos then "00" ++ m else m
     | p              =>
       let m1 := mangleAux p
       m1 ++ (if needDisambiguation p m then "_00" else "_") ++ m
@@ -149,9 +149,9 @@ public def mkPackageSymbolPrefix (pkg? : Option PkgId) : String :=
   pkg?.elim "l_" (s!"lp_{·.mangle}_")
 
 -- assumes `s` has been generated `Name.mangle n ""`
-def Name.demangleAux (s : String) (p₀ : s.Pos) (res : Name)
+def Name.demangleAux (s : String) (p₀ : s.ValidPos) (res : Name)
     (acc : String) (ucount : Nat) : Name :=
-  if hp₀ : p₀ = s.endPos then res.str (acc.pushn '_' (ucount / 2)) else
+  if hp₀ : p₀ = s.endValidPos then res.str (acc.pushn '_' (ucount / 2)) else
   let ch := p₀.get hp₀
   let p := p₀.next hp₀
   if ch = '_' then demangleAux s p res acc (ucount + 1) else
@@ -159,7 +159,7 @@ def Name.demangleAux (s : String) (p₀ : s.Pos) (res : Name)
     demangleAux s p res (acc.pushn '_' (ucount / 2) |>.push ch) 0
   else if ch.isDigit then
     let res := res.str (acc.pushn '_' (ucount / 2))
-    if h : ch = '0' ∧ ∃ h : p ≠ s.endPos, p.get h = '0' then
+    if h : ch = '0' ∧ ∃ h : p ≠ s.endValidPos, p.get h = '0' then
       demangleAux s (p.next h.2.1) res "" 0
     else
       decodeNum s p res (ch.val - 48).toNat
@@ -167,40 +167,40 @@ def Name.demangleAux (s : String) (p₀ : s.Pos) (res : Name)
     match ch, h₁ : parseLowerHex? 2 s p 0 with
     | 'x', some (q, v) =>
       let acc := acc.pushn '_' (ucount / 2)
-      have : p₀ < q := String.Pos.lt_trans p₀.lt_next (lt_of_parseLowerHex?_eq_some (by decide) h₁)
+      have : p₀ < q := String.ValidPos.lt_trans p₀.lt_next (lt_of_parseLowerHex?_eq_some (by decide) h₁)
       demangleAux s q res (acc.push (Char.ofNat v)) 0
     | _, _ =>
       match ch, h₂ : parseLowerHex? 4 s p 0 with
       | 'u', some (q, v) =>
         let acc := acc.pushn '_' (ucount / 2)
-        have : p₀ < q := String.Pos.lt_trans p₀.lt_next (lt_of_parseLowerHex?_eq_some (by decide) h₂)
+        have : p₀ < q := String.ValidPos.lt_trans p₀.lt_next (lt_of_parseLowerHex?_eq_some (by decide) h₂)
         demangleAux s q res (acc.push (Char.ofNat v)) 0
       | _, _ =>
         match ch, h₃ : parseLowerHex? 8 s p 0 with
         | 'U', some (q, v) =>
           let acc := acc.pushn '_' (ucount / 2)
-          have : p₀ < q := String.Pos.lt_trans p₀.lt_next (lt_of_parseLowerHex?_eq_some (by decide) h₃)
+          have : p₀ < q := String.ValidPos.lt_trans p₀.lt_next (lt_of_parseLowerHex?_eq_some (by decide) h₃)
           demangleAux s q res (acc.push (Char.ofNat v)) 0
         | _, _ => demangleAux s p (res.str acc) ("".pushn '_' (ucount / 2) |>.push ch) 0
 termination_by p₀
 where
-  decodeNum (s : String) (p : s.Pos) (res : Name) (n : Nat) : Name :=
-    if h : p = s.endPos then res.num n else
+  decodeNum (s : String) (p : s.ValidPos) (res : Name) (n : Nat) : Name :=
+    if h : p = s.endValidPos then res.num n else
     let ch := p.get h
     let p := p.next h
     if ch.isDigit then
       decodeNum s p res (n * 10 + (ch.val - 48).toNat)
     else -- assume ch = '_'
       let res := res.num n
-      if h : p = s.endPos then res else
+      if h : p = s.endValidPos then res else
       nameStart s (p.next h) res -- assume s.get' p h = '_'
   termination_by p
-  nameStart (s : String) (p : s.Pos) (res : Name) : Name :=
-    if h : p = s.endPos then res else
+  nameStart (s : String) (p : s.ValidPos) (res : Name) : Name :=
+    if h : p = s.endValidPos then res else
     let ch := p.get h
     let p := p.next h
     if ch.isDigit then
-      if h : ch = '0' ∧ ∃ h : p ≠ s.endPos, p.get h = '0' then
+      if h : ch = '0' ∧ ∃ h : p ≠ s.endValidPos, p.get h = '0' then
         demangleAux s (p.next h.2.1) res "" 0
       else
         decodeNum s p res (ch.val - 48).toNat
@@ -212,7 +212,7 @@ where
 
 /-- Assuming `s` has been produced by `Name.mangle _ ""`, return the original name. -/
 public def Name.demangle (s : String) : Name :=
-  demangleAux.nameStart s s.startPos .anonymous
+  demangleAux.nameStart s s.startValidPos .anonymous
 
 /--
 Returns the demangled version of `s`, if it's the result of `Name.mangle _ ""`. Otherwise returns

src/Lean/CoreM.lean

@@ -522,7 +522,7 @@ instance : MonadLog CoreM where
     if (← read).suppressElabErrors then
       -- discard elaboration errors, except for a few important and unlikely misleading ones, on
       -- parse error
-      unless msg.data.hasTag (· matches `Elab.synthPlaceholder | `Tactic.unsolvedGoals | `lean.inductionWithNoAlts._namedError | `trace) do
+      unless msg.data.hasTag (· matches `Elab.synthPlaceholder | `Tactic.unsolvedGoals | `trace) do
         return
 
     let ctx ← read

src/Lean/Data/AssocList.lean

@@ -110,7 +110,7 @@ def all (p : α → β → Bool) : AssocList α β → Bool
       | ForInStep.yield d => loop d es
   loop init as
 
-instance [Monad m] : ForIn m (AssocList α β) (α × β) where
+instance : ForIn m (AssocList α β) (α × β) where
   forIn := AssocList.forIn
 
 end Lean.AssocList

src/Lean/Data/EditDistance.lean

@@ -32,11 +32,11 @@ public def levenshtein (str1 str2 : String) (cutoff : Nat) : Option Nat := Id.ru
 
   for h : i in [0:v0.size] do
     v0 := v0.set i i
-  let mut iter1 := str1.startPos
+  let mut iter1 := str1.startValidPos
   let mut i := 0
   while h1 : ¬iter1.IsAtEnd do
     v1 := v1.set 0 (i+1)
-    let mut iter2 := str2.startPos
+    let mut iter2 := str2.startValidPos
     let mut j : Fin (len2 + 1) := 0
     while h2 : ¬iter2.IsAtEnd do
       let j' : Fin _ := j + 1

src/Lean/Data/KVMap.lean

@@ -183,7 +183,7 @@ def updateSyntax (m : KVMap) (k : Name) (f : Syntax → Syntax) : KVMap :=
   (kv : KVMap) (init : δ) (f : Name × DataValue → δ → m (ForInStep δ)) : m δ :=
   forIn kv.entries init f
 
-instance [Monad m] : ForIn m KVMap (Name × DataValue) where
+instance : ForIn m KVMap (Name × DataValue) where
   forIn := KVMap.forIn
 
 def subsetAux : List (Name × DataValue) → KVMap → Bool

src/Lean/Data/Lsp/Internal.lean

@@ -188,7 +188,7 @@ instance : FromJson RefInfo where
 @[expose] def ModuleRefs := Std.TreeMap RefIdent RefInfo
   deriving EmptyCollection
 
-instance [Monad m] : ForIn m ModuleRefs (RefIdent × RefInfo) where
+instance : ForIn m ModuleRefs (RefIdent × RefInfo) where
   forIn map init f :=
     let map : Std.TreeMap RefIdent RefInfo := map
     forIn map init f

src/Lean/Data/Lsp/Utf16.lean

@@ -9,7 +9,6 @@ module
 prelude
 public import Lean.Data.Lsp.BasicAux
 public import Lean.DeclarationRange
-import Init.Data.String.Search
 
 public section
 

src/Lean/Data/NameMap/Basic.lean

@@ -35,7 +35,7 @@ def contains (m : NameMap α) (n : Name) : Bool := Std.TreeMap.contains m n
 
 def find? (m : NameMap α) (n : Name) : Option α := Std.TreeMap.get? m n
 
-instance [Monad m] : ForIn m (NameMap α) (Name × α) :=
+instance : ForIn m (NameMap α) (Name × α) :=
   inferInstanceAs (ForIn _ (Std.TreeMap _ _ _) ..)
 
 /-- `filter f m` returns the `NameMap` consisting of all
@@ -52,7 +52,7 @@ instance : EmptyCollection NameSet := ⟨empty⟩
 instance : Inhabited NameSet := ⟨empty⟩
 def insert (s : NameSet) (n : Name) : NameSet := Std.TreeSet.insert s n
 def contains (s : NameSet) (n : Name) : Bool := Std.TreeSet.contains s n
-instance [Monad m] : ForIn m NameSet Name :=
+instance : ForIn m NameSet Name :=
   inferInstanceAs (ForIn _ (Std.TreeSet _ _) ..)
 
 /-- The union of two `NameSet`s. -/

src/Lean/Data/Options.lean

@@ -20,27 +20,16 @@ def Options.empty : Options  := {}
 instance : Inhabited Options where
   default := {}
 instance : ToString Options := inferInstanceAs (ToString KVMap)
-instance [Monad m] : ForIn m Options (Name × DataValue) := inferInstanceAs (ForIn _ KVMap _)
+instance : ForIn m Options (Name × DataValue) := inferInstanceAs (ForIn _ KVMap _)
 instance : BEq Options := inferInstanceAs (BEq KVMap)
 
 structure OptionDecl where
-  name     : Name
   declName : Name := by exact decl_name%
   defValue : DataValue
+  group    : String := ""
   descr    : String := ""
   deriving Inhabited
 
-def OptionDecl.fullDescr (self : OptionDecl) : String := Id.run do
-  let mut descr := self.descr
-  if (`backward).isPrefixOf self.name then
-    unless descr.isEmpty do
-      descr := descr ++ "\n\n"
-    descr := descr ++ "\
-      This is a backwards compatibility option, intended to help migrating to new Lean releases. \
-      It may be removed without further notice 6 months after their introduction. \
-      Please report an issue if you rely on this option."
-  pure descr
-
 @[expose] def OptionDecls := NameMap OptionDecl
 
 instance : Inhabited OptionDecls := ⟨({} : NameMap OptionDecl)⟩
@@ -123,6 +112,7 @@ namespace Option
 
 protected structure Decl (α : Type) where
   defValue : α
+  group    : String := ""
   descr    : String := ""
 
 protected def get? [KVMap.Value α] (opts : Options) (opt : Lean.Option α) : Option α :=
@@ -143,9 +133,9 @@ protected def setIfNotSet [KVMap.Value α] (opts : Options) (opt : Lean.Option
 
 protected def register [KVMap.Value α] (name : Name) (decl : Lean.Option.Decl α) (ref : Name := by exact decl_name%) : IO (Lean.Option α) := do
   registerOption name {
-    name
     declName := ref
     defValue := KVMap.Value.toDataValue decl.defValue
+    group := decl.group
     descr := decl.descr
   }
   return { name := name, defValue := decl.defValue }

src/Lean/Data/PersistentArray.lean

@@ -252,7 +252,7 @@ partial def forInAux {α : Type u} {β : Type v} {m : Type v → Type w} [Monad
       | ForInStep.yield bNew => b := bNew
     return b
 
-instance [Monad m] : ForIn m (PersistentArray α) α where
+instance : ForIn m (PersistentArray α) α where
   forIn := PersistentArray.forIn
 
 @[specialize] partial def findSomeMAux (f : α → m (Option β)) : PersistentArrayNode α → m (Option β)

src/Lean/Data/PersistentHashMap.lean

@@ -304,7 +304,7 @@ protected def forIn {_ : BEq α} {_ : Hashable α} [Monad m]
   match result with
   | .ok s | .error s => pure s
 
-instance {_ : BEq α} {_ : Hashable α} [Monad m] : ForIn m (PersistentHashMap α β) (α × β) where
+instance {_ : BEq α} {_ : Hashable α} : ForIn m (PersistentHashMap α β) (α × β) where
   forIn := PersistentHashMap.forIn
 
 end

src/Lean/Data/PersistentHashSet.lean

@@ -61,7 +61,7 @@ protected def forIn {_ : BEq α} {_ : Hashable α} [Monad m]
     (s : PersistentHashSet α) (init : σ) (f : α → σ → m (ForInStep σ)) : m σ := do
   PersistentHashMap.forIn s.set init fun p s => f p.1 s
 
-instance {_ : BEq α} {_ : Hashable α} [Monad m] : ForIn m (PersistentHashSet α) α where
+instance {_ : BEq α} {_ : Hashable α} : ForIn m (PersistentHashSet α) α where
   forIn := PersistentHashSet.forIn
 
 end PersistentHashSet

src/Lean/Data/RBMap.lean

@@ -295,7 +295,7 @@ def isSingleton (t : RBMap α β cmp) : Bool :=
 @[inline] protected def forIn [Monad m] (t : RBMap α β cmp) (init : σ) (f : (α × β) → σ → m (ForInStep σ)) : m σ :=
   t.val.forIn init (fun a b acc => f (a, b) acc)
 
-instance [Monad m] : ForIn m (RBMap α β cmp) (α × β) where
+instance : ForIn m (RBMap α β cmp) (α × β) where
   forIn := RBMap.forIn
 
 @[inline] def isEmpty : RBMap α β cmp → Bool

src/Lean/Data/RBTree.lean

@@ -48,7 +48,7 @@ variable {α : Type u} {β : Type v} {cmp : α → α → Ordering}
 @[inline] protected def forIn [Monad m] (t : RBTree α cmp) (init : σ) (f : α → σ → m (ForInStep σ)) : m σ :=
   t.val.forIn init (fun a _ acc => f a acc)
 
-instance [Monad m] : ForIn m (RBTree α cmp) α where
+instance : ForIn m (RBTree α cmp) α where
   forIn := RBTree.forIn
 
 @[inline] def isEmpty (t : RBTree α cmp) : Bool :=

src/Lean/Data/SMap.lean

@@ -80,10 +80,10 @@ def forM [Monad m] (s : SMap α β) (f : α → β → m PUnit) : m PUnit := do
   s.map₁.forM f
   s.map₂.forM f
 
-instance [Monad m] : ForM m (SMap α β) (α × β) where
+instance : ForM m (SMap α β) (α × β) where
   forM s f := forM s fun x y => f (x, y)
 
-instance [Monad m] : ForIn m (SMap α β) (α × β) where
+instance : ForIn m (SMap α β) (α × β) where
   forIn := ForM.forIn
 
 /-- Move from stage 1 into stage 2. -/

src/Lean/Data/Xml/Parser.lean

@@ -8,7 +8,6 @@ module
 prelude
 public import Std.Internal.Parsec
 public import Lean.Data.Xml.Basic
-import Init.Data.String.Search
 
 public section
 

src/Lean/DocString/Links.lean

@@ -106,7 +106,7 @@ def rewriteManualLinksCore (s : String) : Id (Array (Lean.Syntax.Range × String
   let scheme := "lean-manual://"
   let mut out := ""
   let mut errors := #[]
-  let mut iter := s.startPos
+  let mut iter := s.startValidPos
   while h : ¬iter.IsAtEnd do
     let c := iter.get h
     let pre := iter
@@ -155,7 +155,7 @@ where
   /--
   Returns `true` if `goal` is a prefix of the string at the position pointed to by `iter`.
   -/
-  lookingAt (goal : String) {s : String} (iter : s.Pos) : Bool :=
+  lookingAt (goal : String) {s : String} (iter : s.ValidPos) : Bool :=
     String.Pos.Raw.substrEq s iter.offset goal 0 goal.rawEndPos.byteIdx
 
 /--

src/Lean/DocString/Markdown.lean

@@ -151,7 +151,7 @@ public instance : MarkdownBlock i Empty where
 
 private def escape (s : String) : String := Id.run do
   let mut s' := ""
-  let mut iter := s.startPos
+  let mut iter := s.startValidPos
   while h : ¬iter.IsAtEnd do
     let c := iter.get h
     iter := iter.next h
@@ -165,7 +165,7 @@ where
 private def quoteCode (str : String) : String := Id.run do
   let mut longest := 0
   let mut current := 0
-  let mut iter := str.startPos
+  let mut iter := str.startValidPos
   while h : ¬iter.IsAtEnd do
     let c := iter.get h
     iter := iter.next h
@@ -183,7 +183,7 @@ where
   go : List (Inline i) → String × Inline i
     | [] => ("", .empty)
     | .text s :: more =>
-      if s.all Char.isWhitespace then
+      if s.all (·.isWhitespace) then
         let (pre, post) := go more
         (s ++ pre, post)
       else
@@ -198,7 +198,7 @@ where
   go : List (Inline i) → Inline i × String
     | [] => (.empty, "")
     | .text s :: more =>
-      if s.all Char.isWhitespace then
+      if s.all (·.isWhitespace) then
         let (pre, post) := go more
         (pre, post ++ s)
       else
@@ -273,7 +273,7 @@ public instance [MarkdownInline i] : ToMarkdown (Inline i) where
 private def quoteCodeBlock (indent : Nat) (str : String) : String := Id.run do
   let mut longest := 2
   let mut current := 0
-  let mut iter := str.startPos
+  let mut iter := str.startValidPos
   let mut out := ""
   while h : ¬iter.IsAtEnd do
     let c := iter.get h

src/Lean/DocString/Parser.lean

@@ -123,7 +123,7 @@ private def withInfoSyntaxFn (p : ParserFn) (infoP : SourceInfo → ParserFn) :
 
 private def unescapeStr (str : String) : String := Id.run do
   let mut out := ""
-  let mut iter := str.startPos
+  let mut iter := str.startValidPos
   while h : ¬iter.IsAtEnd do
     let c := iter.get h
     iter := iter.next h
@@ -246,7 +246,7 @@ private def pushMissing : ParserFn := fun _c s =>
   s.pushSyntax .missing
 
 private def strFn (str : String) : ParserFn := asStringFn <| fun c s =>
-  let rec go (iter : str.Pos) (s : ParserState) :=
+  let rec go (iter : str.ValidPos) (s : ParserState) :=
     if h : iter.IsAtEnd then s
     else
       let ch := iter.get h
@@ -254,7 +254,7 @@ private def strFn (str : String) : ParserFn := asStringFn <| fun c s =>
   termination_by iter
   let iniPos := s.pos
   let iniSz := s.stxStack.size
-  let s := go str.startPos s
+  let s := go str.startValidPos s
   if s.hasError then s.mkErrorAt s!"'{str}'" iniPos (some iniSz) else s
 
 /--

src/Lean/Elab.lean

@@ -46,7 +46,6 @@ public import Lean.Elab.Notation
 public import Lean.Elab.Mixfix
 public import Lean.Elab.MacroRules
 public import Lean.Elab.BuiltinCommand
-public import Lean.Elab.Command.WithWeakNamespace
 public import Lean.Elab.BuiltinEvalCommand
 public import Lean.Elab.RecAppSyntax
 public import Lean.Elab.Eval
@@ -63,4 +62,3 @@ public import Lean.Elab.InfoTrees
 public import Lean.Elab.ErrorExplanation
 public import Lean.Elab.DocString
 public import Lean.Elab.DocString.Builtin
-public import Lean.Elab.Parallel

src/Lean/Elab/Command/WithWeakNamespace.lean

@@ -1,40 +0,0 @@
-/-
-Copyright (c) 2021 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mario Carneiro, Daniel Selsam, Gabriel Ebner
--/
-module
-
-prelude
-public import Lean.Elab.Command
-public import Lean.Data.OpenDecl
-
-namespace Lean.Elab.Command
-
-/-- Adds the name to the namespace, `_root_`-aware.
-```
-resolveNamespaceRelative `A `B.b == `A.B.b
-resolveNamespaceRelative `A `_root_.B.c == `B.c
-```
--/
-def resolveNamespaceRelative (ns : Name) : Name → Name
-  | `_root_ => Name.anonymous
-  | Name.str n s .. => Name.mkStr (resolveNamespaceRelative ns n) s
-  | Name.num n i .. => Name.mkNum (resolveNamespaceRelative ns n) i
-  | Name.anonymous => ns
-
-/-- Changes the current namespace without causing scoped things to go out of scope -/
-def withWeakNamespace {α : Type} (ns : Name) (m : CommandElabM α) : CommandElabM α := do
-  let old ← getCurrNamespace
-  let ns := resolveNamespaceRelative old ns
-  modify fun s ↦ { s with env := s.env.registerNamespace ns }
-  modifyScope ({ · with currNamespace := ns })
-  try m finally modifyScope ({ · with currNamespace := old })
-
-@[builtin_command_elab Parser.Command.withWeakNamespace]
-def elabWithWeakNamespace : CommandElab
-  | `(Parser.Command.withWeakNamespace| with_weak_namespace $ns:ident $cmd) =>
-    withWeakNamespace ns.getId (elabCommand cmd)
-  | _ => throwUnsupportedSyntax
-
-end Lean.Elab.Command

src/Lean/Elab/Parallel.lean

@@ -1,665 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kim Morrison
--/
-module
-
-prelude
-public import Lean.Elab.Task
-import Init.System.IO
-
-/-!
-# Iterator-based parallelization for Lean's tactic monads.
-
-This file provides utilities for running computations in parallel using Lean's task system,
-with support for collecting results in different ways.
-
-## Main functions
-
-For each monad (`IO`, `CoreM`, `MetaM`, `TermElabM`, `TacticM`), the following functions are provided:
-
-- `par` / `par'`
-  - Run jobs in parallel, collect results in original order
-  - Takes `List (MonadM α)`, returns `MonadM (List (Except Error (α × State)))` / `MonadM (List (Except Error α))`
-  - All tasks run in parallel, results returned in input order
-  - `par` returns state information, `par'` discards state
-  - Final state is restored to initial state (before tasks ran)
-  - Errors wrapped in `Except` so all results are collected
-
-- `parIter` / `parIterWithCancel`
-  - Run jobs in parallel, iterate over results in original order
-  - Takes `List (MonadM α)`, returns iterator
-  - `parIterWithCancel` also returns cancellation hook
-
-- `parIterGreedy` / `parIterGreedyWithCancel`
-  - Run jobs in parallel, iterate over results in completion order (greedily)
-  - Takes `List (MonadM α)`, returns iterator
-  - `parIterGreedyWithCancel` also returns cancellation hook
-
-- `parFirst`
-  - Run jobs in parallel, return first successful result (by completion order)
-  - Cancels remaining tasks after first success (by default)
-  - Throws error if all tasks fail
-
-## Implementation notes
-
-The greedy iterator-based functions use `IO.waitAny'` internally to wait for task completion in any order.
-The ordered iterator-based functions process tasks sequentially in the original order.
-
-**State threading in iterators:**
-The iterators (`parIter`, `parIterGreedy`, and their `WithCancel` variants) preserve state from each
-completed task. When you map over an iterator with a monadic function, the monad state will be that at
-the conclusion of the monadic action that produced each value. This means:
-- For `parIter`: State is threaded sequentially in the original task order
-- For `parIterGreedy`: State is threaded in task completion order
-
-This allows you to observe state changes (like logged messages, modified metavariable contexts, etc.)
-as tasks complete, unlike `par`/`par'` which restore the initial state after collecting all results.
-
-Iterators do not have `Finite` instances, as we cannot prove termination from the available
-information. For consumers that require `Finite` (like `.toList`), use `.allowNontermination.toList`.
--/
-
-public section
-
-namespace Std.Iterators
-
-/--
-Internal state for an iterator over tasks.
-Maintains the list of tasks that haven't completed yet.
--/
-structure TaskIterator (α : Type w) where
-  private tasks : List (Task α)
-
-private instance {α : Type} : Iterator (TaskIterator α) BaseIO α where
-  IsPlausibleStep it
-    | .yield it' out => True
-    | .skip _ => False
-    | .done => it.internalState.tasks = []
-  step it := do
-    match h : it.internalState.tasks with
-    | [] =>
-        pure <| .deflate ⟨.done, rfl⟩
-    | task :: rest =>
-        have hlen : 0 < (task :: rest).length := by simp
-        let (result, remaining) ← IO.waitAny' (task :: rest) hlen
-        pure <| .deflate ⟨
-          .yield (Std.Iterators.toIterM { tasks := remaining } BaseIO α) result,
-          trivial⟩
-
-end Std.Iterators
-
-namespace IO
-
-open Std.Iterators
-
-/--
-Creates an iterator over a list of tasks that yields results in completion order.
-
-Uses `IO.waitAny'` to wait for the next task to complete (whichever finishes first),
-then yields that result and continues with the remaining tasks.
-
-The iterator will terminate once all tasks have completed, but we don't provide a `Finite`
-instance since we cannot prove termination from the available information.
-In practice, if all tasks eventually complete, the iterator will be finite.
-
-## Example
-```lean
-let tasks : List (Task Nat) ← [
-  IO.asTask (pure 1),
-  IO.asTask (pure 2),
-  IO.asTask (pure 3)
-]
-let iter := IO.iterTasks tasks
-for result in iter do
-  IO.println s!"Got result: {result}"
-```
--/
-private def iterTasks {α : Type} (tasks : List (Task α)) : IterM (α := TaskIterator α) BaseIO α :=
-  Std.Iterators.toIterM { tasks } BaseIO α
-
-end IO
-
-namespace Lean.Core.CoreM
-
-open Std.Iterators
-
-/--
-Runs a list of CoreM computations in parallel and returns:
-* a combined cancellation hook for all tasks, and
-* an iterator that yields results in original order.
-
-The iterator runs in CoreM, and as it yields each result, it updates the CoreM state
-to reflect the state when that particular task completed. This means the state is
-threaded through the iteration in the order of the original list.
-
-Results are wrapped in `Except Exception α` so that errors in individual tasks don't stop
-the iteration - you can observe all results including which tasks failed.
-
-The iterator will terminate after all jobs complete (assuming they all do complete).
--/
-def parIterWithCancel {α : Type} (jobs : List (CoreM α)) := do
-  let (cancels, tasks) := (← jobs.mapM asTask).unzip
-  let combinedCancel := cancels.forM id
-  let iterWithErrors := tasks.iter.mapM fun (task : Task (CoreM α)) => do
-    try
-      let result ← task.get
-      pure (Except.ok result)
-    catch e =>
-      pure (Except.error e)
-  return (combinedCancel, iterWithErrors)
-
-/--
-Runs a list of CoreM computations in parallel (without cancellation hook).
-
-Returns an iterator that yields results in original order, wrapped in `Except Exception α`.
--/
-def parIter {α : Type} (jobs : List (CoreM α)) :=
-  (·.2) <$> parIterWithCancel jobs
-
-/--
-Runs a list of CoreM computations in parallel and returns:
-* a combined cancellation hook for all tasks, and
-* an iterator that yields results in completion order (greedily).
-
-The iterator runs in CoreM, and as it yields each result, it updates the CoreM state
-to reflect the state when that particular task completed. This means the state is
-threaded through the iteration in task completion order.
-
-Results are wrapped in `Except Exception α` so that errors in individual tasks don't stop
-the iteration - you can observe all results including which tasks failed.
-
-The iterator will terminate after all jobs complete (assuming they all do complete).
--/
-def parIterGreedyWithCancel {α : Type} (jobs : List (CoreM α)) := do
-  let (cancels, tasks) := (← jobs.mapM asTask).unzip
-  let combinedCancel := cancels.forM id
-  let baseIter := IO.iterTasks tasks
-  -- mapM with error handling - execute each task and catch errors
-  let iterWithErrors := baseIter.mapM fun taskMonadic => do
-    try
-      pure (Except.ok (← taskMonadic))
-    catch e =>
-      pure (Except.error e)
-  return (combinedCancel, iterWithErrors)
-
-/--
-Runs a list of CoreM computations in parallel (without cancellation hook).
-
-Returns an iterator that yields results in completion order, wrapped in `Except Exception α`.
--/
-def parIterGreedy {α : Type} (jobs : List (CoreM α)) :=
-  (·.2) <$> parIterGreedyWithCancel jobs
-
-/--
-Runs a list of CoreM computations in parallel and collects results in the original order,
-including the saved state after each task completes.
-
-Unlike `parIter`, this waits for all tasks to complete and returns results
-in the same order as the input list, not in completion order.
-
-Results are wrapped in `Except Exception (α × Core.SavedState)` so that errors in individual
-tasks don't stop the collection - you can observe all results including which tasks failed.
-
-The final CoreM state is restored to the initial state (before tasks ran).
--/
-def par {α : Type} (jobs : List (CoreM α)) : CoreM (List (Except Exception (α × Core.SavedState))) := do
-  let initialState ← get
-  let tasks ← jobs.mapM asTask'
-  let mut results := []
-  for task in tasks do
-    let resultWithState ← observing do
-      let result ← task.get
-      pure (result, (← saveState))
-    results := resultWithState :: results
-  set initialState
-  return results.reverse
-
-/--
-Runs a list of CoreM computations in parallel and collects results in the original order,
-discarding state information.
-
-Unlike `par`, this doesn't return state information from tasks.
-
-The final CoreM state is restored to the initial state (before tasks ran).
--/
-def par' {α : Type} (jobs : List (CoreM α)) : CoreM (List (Except Exception α)) := do
-  let initialState ← get
-  let tasks ← jobs.mapM asTask'
-  let mut results := []
-  for task in tasks do
-    try
-      let result ← task.get
-      results := .ok result :: results
-    catch e =>
-      results := .error e :: results
-  set initialState
-  return results.reverse
-
-/--
-Runs a list of CoreM computations in parallel and returns the first successful result
-(by completion order, not list order).
-
-If `cancel := true` (the default), cancels all remaining tasks after the first success.
--/
-def parFirst {α : Type} (jobs : List (CoreM α)) (cancel : Bool := true) : CoreM α := do
-  let (cancelHook, iter) ← parIterGreedyWithCancel jobs
-  for result in iter.allowNontermination do
-    match result with
-    | .ok value =>
-      if cancel then cancelHook
-      return value
-    | .error _ => continue
-  throwError "All parallel tasks failed"
-
-end Lean.Core.CoreM
-
-namespace Lean.Meta.MetaM
-
-open Std.Iterators
-
-/--
-Runs a list of MetaM computations in parallel and collects results in the original order,
-including the saved state after each task completes.
-
-Unlike `parIter`, this waits for all tasks to complete and returns results
-in the same order as the input list, not in completion order.
-
-Results are wrapped in `Except Exception (α × Meta.SavedState)` so that errors in individual
-tasks don't stop the collection - you can observe all results including which tasks failed.
-
-The final MetaM state is restored to the initial state (before tasks ran).
--/
-def par {α : Type} (jobs : List (MetaM α)) : MetaM (List (Except Exception (α × Meta.SavedState))) := do
-  let initialState ← get
-  let tasks ← jobs.mapM asTask'
-  let mut results := []
-  for task in tasks do
-    let resultWithState ← observing do
-      let result ← task.get
-      pure (result, (← saveState))
-    results := resultWithState :: results
-  set initialState
-  return results.reverse
-
-/--
-Runs a list of MetaM computations in parallel and collects results in the original order,
-discarding state information.
-
-Unlike `par`, this doesn't return state information from tasks.
-
-The final MetaM state is restored to the initial state (before tasks ran).
--/
-def par' {α : Type} (jobs : List (MetaM α)) : MetaM (List (Except Exception α)) := do
-  let initialState ← get
-  let tasks ← jobs.mapM asTask'
-  let mut results := []
-  for task in tasks do
-    try
-      let result ← task.get
-      results := .ok result :: results
-    catch e =>
-      results := .error e :: results
-  set initialState
-  return results.reverse
-
-/--
-Runs a list of MetaM computations in parallel and returns:
-* a combined cancellation hook for all tasks, and
-* an iterator that yields results in original order.
-
-The iterator runs in MetaM, and as it yields each result, it updates the MetaM state
-to reflect the state when that particular task completed. This means the state is
-threaded through the iteration in the order of the original list.
-
-Results are wrapped in `Except Exception α` so that errors in individual tasks don't stop
-the iteration - you can observe all results including which tasks failed.
-
-The iterator will terminate after all jobs complete (assuming they all do complete).
--/
-def parIterWithCancel {α : Type} (jobs : List (MetaM α)) := do
-  let (cancels, tasks) := (← jobs.mapM asTask).unzip
-  let combinedCancel := cancels.forM id
-  -- Create iterator that processes tasks sequentially
-  let iterWithErrors := tasks.iter.mapM fun (task : Task (MetaM α)) => do
-    try
-      let result ← task.get
-      pure (Except.ok result)
-    catch e =>
-      pure (Except.error e)
-  return (combinedCancel, iterWithErrors)
-
-/--
-Runs a list of MetaM computations in parallel (without cancellation hook).
-
-Returns an iterator that yields results in original order, wrapped in `Except Exception α`.
--/
-def parIter {α : Type} (jobs : List (MetaM α)) :=
-  (·.2) <$> parIterWithCancel jobs
-
-/--
-Runs a list of MetaM computations in parallel and returns:
-* a combined cancellation hook for all tasks, and
-* an iterator that yields results in completion order (greedily).
-
-The iterator runs in MetaM, and as it yields each result, it updates the MetaM state
-to reflect the state when that particular task completed. This means the state is
-threaded through the iteration in task completion order.
-
-Results are wrapped in `Except Exception α` so that errors in individual tasks don't stop
-the iteration - you can observe all results including which tasks failed.
-
-The iterator will terminate after all jobs complete (assuming they all do complete).
--/
-def parIterGreedyWithCancel {α : Type} (jobs : List (MetaM α)) := do
-  let (cancels, tasks) := (← jobs.mapM asTask).unzip
-  let combinedCancel := cancels.forM id
-  let baseIter := IO.iterTasks tasks
-  -- mapM with error handling - execute each task and catch errors
-  let iterWithErrors := baseIter.mapM fun taskMonadic => do
-    try
-      pure (Except.ok (← taskMonadic))
-    catch e =>
-      pure (Except.error e)
-  return (combinedCancel, iterWithErrors)
-
-/--
-Runs a list of MetaM computations in parallel (without cancellation hook).
-
-Returns an iterator that yields results in completion order, wrapped in `Except Exception α`.
--/
-def parIterGreedy {α : Type} (jobs : List (MetaM α)) :=
-  (·.2) <$> parIterGreedyWithCancel jobs
-
-/--
-Runs a list of MetaM computations in parallel and returns the first successful result
-(by completion order, not list order).
-
-If `cancel := true` (the default), cancels all remaining tasks after the first success.
--/
-def parFirst {α : Type} (jobs : List (MetaM α)) (cancel : Bool := true) : MetaM α := do
-  let (cancelHook, iter) ← parIterGreedyWithCancel jobs
-  for result in iter.allowNontermination do
-    match result with
-    | .ok value =>
-      if cancel then cancelHook
-      return value
-    | .error _ => continue
-  throwError "All parallel tasks failed"
-
-end Lean.Meta.MetaM
-
-namespace Lean.Elab.Term.TermElabM
-
-open Std.Iterators
-
-/--
-Runs a list of TermElabM computations in parallel and returns:
-* a combined cancellation hook for all tasks, and
-* an iterator that yields results in original order.
-
-The iterator runs in TermElabM, and as it yields each result, it updates the TermElabM state
-to reflect the state when that particular task completed. This means the state is
-threaded through the iteration in the order of the original list.
-
-Results are wrapped in `Except Exception α` so that errors in individual tasks don't stop
-the iteration - you can observe all results including which tasks failed.
-
-The iterator will terminate after all jobs complete (assuming they all do complete).
--/
-def parIterWithCancel {α : Type} (jobs : List (TermElabM α)) := do
-  let (cancels, tasks) := (← jobs.mapM asTask).unzip
-  let combinedCancel := cancels.forM id
-  -- Create iterator that processes tasks sequentially
-  let iterWithErrors := tasks.iter.mapM fun (task : Task (TermElabM α)) => do
-    try
-      let result ← task.get
-      pure (Except.ok result)
-    catch e =>
-      pure (Except.error e)
-  return (combinedCancel, iterWithErrors)
-
-/--
-Runs a list of TermElabM computations in parallel (without cancellation hook).
-
-Returns an iterator that yields results in original order, wrapped in `Except Exception α`.
--/
-def parIter {α : Type} (jobs : List (TermElabM α)) :=
-  (·.2) <$> parIterWithCancel jobs
-
-/--
-Runs a list of TermElabM computations in parallel and returns:
-* a combined cancellation hook for all tasks, and
-* an iterator that yields results in completion order (greedily).
-
-The iterator runs in TermElabM, and as it yields each result, it updates the TermElabM state
-to reflect the state when that particular task completed. This means the state is
-threaded through the iteration in task completion order.
-
-Results are wrapped in `Except Exception α` so that errors in individual tasks don't stop
-the iteration - you can observe all results including which tasks failed.
-
-The iterator will terminate after all jobs complete (assuming they all do complete).
--/
-def parIterGreedyWithCancel {α : Type} (jobs : List (TermElabM α)) := do
-  let (cancels, tasks) := (← jobs.mapM asTask).unzip
-  let combinedCancel := cancels.forM id
-  let baseIter := IO.iterTasks tasks
-  -- mapM with error handling - execute each task and catch errors
-  let iterWithErrors := baseIter.mapM fun taskMonadic => do
-    try
-      pure (Except.ok (← taskMonadic))
-    catch e =>
-      pure (Except.error e)
-  return (combinedCancel, iterWithErrors)
-
-/--
-Runs a list of TermElabM computations in parallel (without cancellation hook).
-
-Returns an iterator that yields results in completion order, wrapped in `Except Exception α`.
--/
-def parIterGreedy {α : Type} (jobs : List (TermElabM α)) :=
-  (·.2) <$> parIterGreedyWithCancel jobs
-
-/--
-Runs a list of TermElabM computations in parallel and collects results in the original order,
-including the saved state after each task completes.
-
-Unlike `parIter`, this waits for all tasks to complete and returns results
-in the same order as the input list, not in completion order.
-
-Results are wrapped in `Except Exception (α × Term.SavedState)` so that errors in individual
-tasks don't stop the collection - you can observe all results including which tasks failed.
-
-The final TermElabM state is restored to the initial state (before tasks ran).
--/
-def par {α : Type} (jobs : List (TermElabM α)) : TermElabM (List (Except Exception (α × Term.SavedState))) := do
-  let initialState ← get
-  let tasks ← jobs.mapM asTask'
-  let mut results := []
-  for task in tasks do
-    try
-      let result ← task.get
-      let taskState ← saveState
-      results := .ok (result, taskState) :: results
-    catch e =>
-      results := .error e :: results
-  set initialState
-  return results.reverse
-
-/--
-Runs a list of TermElabM computations in parallel and collects results in the original order,
-discarding state information.
-
-Unlike `par`, this doesn't return state information from tasks.
-
-The final TermElabM state is restored to the initial state (before tasks ran).
--/
-def par' {α : Type} (jobs : List (TermElabM α)) : TermElabM (List (Except Exception α)) := do
-  let initialState ← get
-  let tasks ← jobs.mapM asTask'
-  let mut results := []
-  for task in tasks do
-    try
-      let result ← task.get
-      results := .ok result :: results
-    catch e =>
-      results := .error e :: results
-  set initialState
-  return results.reverse
-
-/--
-Runs a list of TermElabM computations in parallel and returns the first successful result
-(by completion order, not list order).
-
-If `cancel := true` (the default), cancels all remaining tasks after the first success.
--/
-def parFirst {α : Type} (jobs : List (TermElabM α)) (cancel : Bool := true) : TermElabM α := do
-  let (cancelHook, iter) ← parIterGreedyWithCancel jobs
-  for result in iter.allowNontermination do
-    match result with
-    | .ok value =>
-      if cancel then cancelHook
-      return value
-    | .error _ => continue
-  throwError "All parallel tasks failed"
-
-end Lean.Elab.Term.TermElabM
-
-namespace Lean.Elab.Tactic.TacticM
-
-open Std.Iterators
-
-/--
-Runs a list of TacticM computations in parallel and returns:
-* a combined cancellation hook for all tasks, and
-* an iterator that yields results in original order.
-
-The iterator runs in TacticM, and as it yields each result, it updates the TacticM state
-to reflect the state when that particular task completed. This means the state is
-threaded through the iteration in the order of the original list.
-
-Results are wrapped in `Except Exception α` so that errors in individual tasks don't stop
-the iteration - you can observe all results including which tasks failed.
-
-The iterator will terminate after all jobs complete (assuming they all do complete).
--/
-def parIterWithCancel {α : Type} (jobs : List (TacticM α)) := do
-  let (cancels, tasks) := (← jobs.mapM asTask).unzip
-  let combinedCancel := cancels.forM id
-  -- Create iterator that processes tasks sequentially
-  let iterWithErrors := tasks.iter.mapM fun (task : Task (TacticM α)) => do
-    try
-      let result ← task.get
-      pure (Except.ok result)
-    catch e =>
-      pure (Except.error e)
-  return (combinedCancel, iterWithErrors)
-
-/--
-Runs a list of TacticM computations in parallel (without cancellation hook).
-
-Returns an iterator that yields results in original order, wrapped in `Except Exception α`.
--/
-def parIter {α : Type} (jobs : List (TacticM α)) :=
-  (·.2) <$> parIterWithCancel jobs
-
-/--
-Runs a list of TacticM computations in parallel and returns:
-* a combined cancellation hook for all tasks, and
-* an iterator that yields results in completion order (greedily).
-
-The iterator runs in TacticM, and as it yields each result, it updates the TacticM state
-to reflect the state when that particular task completed. This means the state is
-threaded through the iteration in task completion order.
-
-Results are wrapped in `Except Exception α` so that errors in individual tasks don't stop
-the iteration - you can observe all results including which tasks failed.
-
-The iterator will terminate after all jobs complete (assuming they all do complete).
--/
-def parIterGreedyWithCancel {α : Type} (jobs : List (TacticM α)) := do
-  let (cancels, tasks) := (← jobs.mapM asTask).unzip
-  let combinedCancel := cancels.forM id
-  let baseIter := IO.iterTasks tasks
-  -- mapM with error handling - execute each task and catch errors
-  let iterWithErrors := baseIter.mapM fun taskMonadic => do
-    try
-      pure (Except.ok (← taskMonadic))
-    catch e =>
-      pure (Except.error e)
-  return (combinedCancel, iterWithErrors)
-
-/--
-Runs a list of TacticM computations in parallel (without cancellation hook).
-
-Returns an iterator that yields results in completion order, wrapped in `Except Exception α`.
--/
-def parIterGreedy {α : Type} (jobs : List (TacticM α)) :=
-  (·.2) <$> parIterGreedyWithCancel jobs
-
-/--
-Runs a list of TacticM computations in parallel and collects results in the original order,
-including the saved state after each task completes.
-
-Unlike `parIter`, this waits for all tasks to complete and returns results
-in the same order as the input list, not in completion order.
-
-Results are wrapped in `Except Exception (α × Tactic.SavedState)` so that errors in individual
-tasks don't stop the collection - you can observe all results including which tasks failed.
-
-The final TacticM state is restored to the initial state (before tasks ran).
--/
-def par {α : Type} (jobs : List (TacticM α)) : TacticM (List (Except Exception (α × Tactic.SavedState))) := do
-  let initialState ← get
-  let tasks ← jobs.mapM asTask'
-  let mut results := []
-  for task in tasks do
-    try
-      let result ← task.get
-      let taskState ← Tactic.saveState
-      results := .ok (result, taskState) :: results
-    catch e =>
-      results := .error e :: results
-  set initialState
-  return results.reverse
-
-/--
-Runs a list of TacticM computations in parallel and collects results in the original order,
-discarding state information.
-
-Unlike `par`, this doesn't return state information from tasks.
-
-The final TacticM state is restored to the initial state (before tasks ran).
--/
-def par' {α : Type} (jobs : List (TacticM α)) : TacticM (List (Except Exception α)) := do
-  let initialState ← get
-  let tasks ← jobs.mapM asTask'
-  let mut results := []
-  for task in tasks do
-    try
-      let result ← task.get
-      results := .ok result :: results
-    catch e =>
-      results := .error e :: results
-  set initialState
-  return results.reverse
-
-/--
-Runs a list of TacticM computations in parallel and returns the first successful result
-(by completion order, not list order).
-
-If `cancel := true` (the default), cancels all remaining tasks after the first success.
--/
-def parFirst {α : Type} (jobs : List (TacticM α)) (cancel : Bool := true) : TacticM α := do
-  let (cancelHook, iter) ← parIterGreedyWithCancel jobs
-  for result in iter.allowNontermination do
-    match result with
-    | .ok value =>
-      if cancel then cancelHook
-      return value
-    | .error _ => continue
-  throwError "All parallel tasks failed"
-
-end Lean.Elab.Tactic.TacticM

src/Lean/Elab/Tactic/Grind/Annotated.lean

@@ -7,7 +7,9 @@ module
 prelude
 public import Lean.Elab.Command
 import Init.Grind.Annotated
-import Std.Time.Format
+public import Std.Time.Format
+
+@[expose] public section
 
 namespace Lean.Elab.Tactic.Grind
 open Command Std.Time
@@ -24,12 +26,6 @@ builtin_initialize grindAnnotatedExt : SimplePersistentEnvExtension Name NameSet
     asyncMode := .sync
   }
 
-/-- Check if a module has been marked as grind-annotated. -/
-public def isGrindAnnotatedModule (env : Environment) (modIdx : ModuleIdx) : Bool :=
-  let state := grindAnnotatedExt.getState env
-  let moduleName := env.header.moduleNames[modIdx.toNat]!
-  state.contains moduleName
-
 @[builtin_command_elab Lean.Parser.Command.grindAnnotated]
 def elabGrindAnnotated : CommandElab := fun stx => do
   let `(grind_annotated $dateStr) := stx | throwUnsupportedSyntax

src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean

@@ -13,7 +13,6 @@ import Lean.Meta.Tactic.Grind.Arith.Linear.Search
 import Lean.Meta.Tactic.Grind.Arith.CommRing.EqCnstr
 import Lean.Meta.Tactic.Grind.AC.Eq
 import Lean.Meta.Tactic.Grind.EMatch
-import Lean.Meta.Tactic.Grind.EMatchTheorem
 import Lean.Meta.Tactic.Grind.PP
 import Lean.Meta.Tactic.Grind.Internalize
 import Lean.Meta.Tactic.Grind.Intro
@@ -153,10 +152,6 @@ def ematchThms (only : Bool) (thms : Array EMatchTheorem) : GrindTacticM Unit :=
   if let some thmRefs := thmRefs? then
     for thmRef in thmRefs do
       match thmRef with
-      | `(Parser.Tactic.Grind.thm| namespace $ns:ident) =>
-        let namespaceName := ns.getId
-        let scopedThms ← Grind.getEMatchTheoremsForNamespace namespaceName
-        thms := thms ++ scopedThms
       | `(Parser.Tactic.Grind.thm| #$anchor:hexnum) => thms := thms ++ (← withRef thmRef <| elabLocalEMatchTheorem anchor)
       | `(Parser.Tactic.Grind.thm| $[$mod?:grindMod]? $id:ident) => thms := thms ++ (← withRef thmRef <| elabThm mod? id false)
       | `(Parser.Tactic.Grind.thm| ! $[$mod?:grindMod]? $id:ident) => thms := thms ++ (← withRef thmRef <| elabThm mod? id true)