chore: remove unnecessary annotation

.github/workflows/build-template.yml

@@ -82,7 +82,7 @@ jobs:
       - name: CI Merge Checkout
         run: |
           git fetch --depth=1 origin ${{ github.sha }}
-          git checkout FETCH_HEAD flake.nix flake.lock script/prepare-*
+          git checkout FETCH_HEAD flake.nix flake.lock
         if: github.event_name == 'pull_request'
       # (needs to be after "Checkout" so files don't get overridden)
       - name: Setup emsdk
@@ -99,6 +99,7 @@ jobs:
         if: matrix.cmultilib
       - name: Cache
         id: restore-cache
+        if: matrix.name != 'Linux Lake'
         uses: actions/cache/restore@v4
         with:
           # NOTE: must be in sync with `save` below

.github/workflows/ci.yml

@@ -139,21 +139,20 @@ jobs:
             let large = ${{ github.repository == 'leanprover/lean4' }};
             const isPr = "${{ github.event_name }}" == "pull_request";
             let matrix = [
-              /* TODO: to be updated to new LLVM
               {
                 "name": "Linux LLVM",
                 "os": "ubuntu-latest",
                 "release": false,
                 "check-level": 2,
                 "shell": "nix develop .#oldGlibc -c bash -euxo pipefail {0}",
-                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-linux-gnu.tar.zst",
+                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-linux-gnu.tar.zst",
                 "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
                 "binary-check": "ldd -v",
                 // foreign code may be linked against more recent glibc
                 // reverse-ffi needs to be updated to link to LLVM libraries
                 "CTEST_OPTIONS": "-E 'foreign|leanlaketest_reverse-ffi'",
                 "CMAKE_OPTIONS": "-DLLVM=ON -DLLVM_CONFIG=${GITHUB_WORKSPACE}/build/llvm-host/bin/llvm-config"
-              }, */
+              },
               {
                 // portable release build: use channel with older glibc (2.26)
                 "name": "Linux release",
@@ -161,23 +160,25 @@ jobs:
                 "release": true,
                 "check-level": 0,
                 "shell": "nix develop .#oldGlibc -c bash -euxo pipefail {0}",
-                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-linux-gnu.tar.zst",
+                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-linux-gnu.tar.zst",
                 "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
                 "binary-check": "ldd -v",
                 // foreign code may be linked against more recent glibc
                 "CTEST_OPTIONS": "-E 'foreign'"
               },
+              // deactivated due to bugs
+              /*
               {
                 "name": "Linux Lake",
                 "os": large ? "nscloud-ubuntu-22.04-amd64-4x8" : "ubuntu-latest",
-                "check-level": 0,
-                // just a secondary build job for now until false positives can be excluded
+                // just a secondary PR build job for now
+                "check-level": isPr ? 0 : 3,
                 "secondary": true,
                 "CMAKE_OPTIONS": "-DUSE_LAKE=ON",
-                // TODO: importStructure is not compatible with .olean caching
-                // TODO: why does scopedMacros fail?
-                "CTEST_OPTIONS": "-E 'scopedMacros|importStructure'"
+                // TODO: why does this fail?
+                "CTEST_OPTIONS": "-E 'scopedMacros'"
               },
+              */
               {
                 "name": "Linux",
                 "os": large ? "nscloud-ubuntu-22.04-amd64-4x8" : "ubuntu-latest",
@@ -209,7 +210,7 @@ jobs:
                 "release": true,
                 "check-level": 2,
                 "shell": "bash -euxo pipefail {0}",
-                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-apple-darwin.tar.zst",
+                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-apple-darwin.tar.zst",
                 "prepare-llvm": "../script/prepare-llvm-macos.sh lean-llvm*",
                 "binary-check": "otool -L",
                 "tar": "gtar" // https://github.com/actions/runner-images/issues/2619
@@ -220,7 +221,7 @@ jobs:
                 "CMAKE_OPTIONS": "-DLEAN_INSTALL_SUFFIX=-darwin_aarch64",
                 "release": true,
                 "shell": "bash -euxo pipefail {0}",
-                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-aarch64-apple-darwin.tar.zst",
+                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-aarch64-apple-darwin.tar.zst",
                 "prepare-llvm": "../script/prepare-llvm-macos.sh lean-llvm*",
                 "binary-check": "otool -L",
                 "tar": "gtar", // https://github.com/actions/runner-images/issues/2619
@@ -241,7 +242,7 @@ jobs:
                 "CMAKE_OPTIONS": "-G \"Unix Makefiles\"",
                 // for reasons unknown, interactivetests are flaky on Windows
                 "CTEST_OPTIONS": "--repeat until-pass:2",
-                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-w64-windows-gnu.tar.zst",
+                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-w64-windows-gnu.tar.zst",
                 "prepare-llvm": "../script/prepare-llvm-mingw.sh lean-llvm*",
                 "binary-check": "ldd"
               },
@@ -252,7 +253,7 @@ jobs:
                 "release": true,
                 "check-level": 2,
                 "shell": "nix develop .#oldGlibcAArch -c bash -euxo pipefail {0}",
-                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-aarch64-linux-gnu.tar.zst",
+                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-aarch64-linux-gnu.tar.zst",
                 "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*"
               },
               // Started running out of memory building expensive modules, a 2GB heap is just not that much even before fragmentation

.github/workflows/nix-ci.yml

@@ -73,7 +73,7 @@ jobs:
         with:
           extra-conf: |
             extra-sandbox-paths = /nix/var/cache/ccache?
-            substituters = file://${{ github.workspace }}/nix-store-cache-copy?priority=10&trusted=true https://cache.nixos.org
+            substituters = file://${{ github.workspace }}/nix-store-cache-copy?priority=10&trusted=true https://cache.nixos.org  
       - name: Prepare CCache Cache
         run: |
           sudo mkdir -m0770 -p /nix/var/cache/ccache
@@ -103,10 +103,40 @@ jobs:
           paths: push-test/test-results.xml
         if: always()
         continue-on-error: true
+      - name: Build manual
+        run: |
+          nix build $NIX_BUILD_ARGS --update-input lean --no-write-lock-file ./doc#{lean-mdbook,leanInk,alectryon,inked} -o push-doc
+          nix build $NIX_BUILD_ARGS --update-input lean --no-write-lock-file ./doc
+          # https://github.com/netlify/cli/issues/1809
+          cp -r --dereference ./result ./dist
+        if: matrix.name == 'Nix Linux'
       - name: Rebuild Nix Store Cache
         run: |
           rm -rf nix-store-cache || true
           nix copy ./push-* --to file://$PWD/nix-store-cache?compression=none
+      - id: deploy-info
+        name: Compute Deployment Metadata
+        run: |
+          set -e
+          python3 -c 'import base64; print("alias="+base64.urlsafe_b64encode(bytes.fromhex("${{github.sha}}")).decode("utf-8").rstrip("="))' >> "$GITHUB_OUTPUT"
+          echo "message=`git log -1 --pretty=format:"%s"`" >> "$GITHUB_OUTPUT"
+      - name: Publish manual to Netlify
+        uses: nwtgck/actions-netlify@v3.0
+        id: publish-manual
+        with:
+          publish-dir: ./dist
+          production-branch: master
+          github-token: ${{ secrets.GITHUB_TOKEN }}
+          deploy-message: |
+            ${{ github.event_name == 'pull_request' && format('pr#{0}: {1}', github.event.number, github.event.pull_request.title) || format('ref/{0}: {1}', github.ref_name, steps.deploy-info.outputs.message) }}
+          alias: ${{ steps.deploy-info.outputs.alias }}
+          enable-commit-comment: false
+          enable-pull-request-comment: false
+          github-deployment-environment: "lean-lang.org/lean4/doc"
+          fails-without-credentials: false
+        env:
+          NETLIFY_AUTH_TOKEN: ${{ secrets.NETLIFY_AUTH_TOKEN }}
+          NETLIFY_SITE_ID: "b8e805d2-7e9b-4f80-91fb-a84d72fc4a68"
       - name: Fixup CCache Cache
         run: |
           sudo chown -R $USER /nix/var/cache

CMakeLists.txt

@@ -5,15 +5,13 @@ option(USE_MIMALLOC "use mimalloc" ON)
 # store all variables passed on the command line into CL_ARGS so we can pass them to the stage builds
 # https://stackoverflow.com/a/48555098/161659
 # MUST be done before call to 'project'
-# Use standard release build (discarding LEAN_EXTRA_CXX_FLAGS etc.) for stage0 by default since it is assumed to be "good", but still pass through CMake platform arguments (compiler, toolchain file, ..).
+# Use standard release build (discarding LEAN_CXX_EXTRA_FLAGS etc.) for stage0 by default since it is assumed to be "good", but still pass through CMake platform arguments (compiler, toolchain file, ..).
 # Use `STAGE0_` prefix to pass variables to stage0 explicitly.
 get_cmake_property(vars CACHE_VARIABLES)
 foreach(var ${vars})
   get_property(currentHelpString CACHE "${var}" PROPERTY HELPSTRING)
   if("${var}" MATCHES "STAGE0_(.*)")
     list(APPEND STAGE0_ARGS "-D${CMAKE_MATCH_1}=${${var}}")
-  elseif("${var}" MATCHES "STAGE1_(.*)")
-    list(APPEND STAGE1_ARGS "-D${CMAKE_MATCH_1}=${${var}}")
   elseif("${currentHelpString}" MATCHES "No help, variable specified on the command line." OR "${currentHelpString}" STREQUAL "")
     list(APPEND CL_ARGS "-D${var}=${${var}}")
     if("${var}" MATCHES "USE_GMP|CHECK_OLEAN_VERSION")
@@ -39,14 +37,10 @@ endif()
 
 # Don't do anything with cadical on wasm
 if (NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
+  # On CI Linux, we source cadical from Nix instead; see flake.nix
   find_program(CADICAL cadical)
   if(NOT CADICAL)
     set(CADICAL_CXX c++)
-    if (CADICAL_USE_CUSTOM_CXX)
-      set(CADICAL_CXX ${CMAKE_CXX_COMPILER})
-      set(CADICAL_CXXFLAGS "${LEAN_EXTRA_CXX_FLAGS}")
-      set(CADICAL_LDFLAGS "-Wl,-rpath=\\$$ORIGIN/../lib")
-    endif()
     find_program(CCACHE ccache)
     if(CCACHE)
       set(CADICAL_CXX "${CCACHE} ${CADICAL_CXX}")
@@ -61,11 +55,8 @@ if (NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
       GIT_REPOSITORY https://github.com/arminbiere/cadical
       GIT_TAG rel-2.1.2
       CONFIGURE_COMMAND ""
-      BUILD_COMMAND $(MAKE) -f ${CMAKE_SOURCE_DIR}/src/cadical.mk
-        CMAKE_EXECUTABLE_SUFFIX=${CMAKE_EXECUTABLE_SUFFIX}
-        CXX=${CADICAL_CXX}
-        CXXFLAGS=${CADICAL_CXXFLAGS}
-        LDFLAGS=${CADICAL_LDFLAGS}
+      # https://github.com/arminbiere/cadical/blob/master/BUILD.md#manual-build
+      BUILD_COMMAND $(MAKE) -f ${CMAKE_SOURCE_DIR}/src/cadical.mk CMAKE_EXECUTABLE_SUFFIX=${CMAKE_EXECUTABLE_SUFFIX} CXX=${CADICAL_CXX} CXXFLAGS=${CADICAL_CXXFLAGS}
       BUILD_IN_SOURCE ON
       INSTALL_COMMAND "")
     set(CADICAL ${CMAKE_BINARY_DIR}/cadical/cadical${CMAKE_EXECUTABLE_SUFFIX} CACHE FILEPATH "path to cadical binary" FORCE)
@@ -86,29 +77,26 @@ if (USE_MIMALLOC)
   list(APPEND EXTRA_DEPENDS mimalloc)
 endif()
 
-if (NOT STAGE1_PREV_STAGE)
-  ExternalProject_add(stage0
-    SOURCE_DIR "${LEAN_SOURCE_DIR}/stage0"
-    SOURCE_SUBDIR src
-    BINARY_DIR stage0
-    # do not rebuild stage0 when git hash changes; it's not from this commit anyway
-    # (however, CI will override this as we need to embed the githash into the stage 1 library built
-    # by stage 0)
-    CMAKE_ARGS -DSTAGE=0 -DUSE_GITHASH=OFF ${PLATFORM_ARGS} ${STAGE0_ARGS}
-    BUILD_ALWAYS ON  # cmake doesn't auto-detect changes without a download method
-    INSTALL_COMMAND ""  # skip install
-    DEPENDS ${EXTRA_DEPENDS}
-  )
-  list(APPEND EXTRA_DEPENDS stage0)
-endif()
+ExternalProject_add(stage0
+  SOURCE_DIR "${LEAN_SOURCE_DIR}/stage0"
+  SOURCE_SUBDIR src
+  BINARY_DIR stage0
+  # do not rebuild stage0 when git hash changes; it's not from this commit anyway
+  # (however, CI will override this as we need to embed the githash into the stage 1 library built
+  # by stage 0)
+  CMAKE_ARGS -DSTAGE=0 -DUSE_GITHASH=OFF ${PLATFORM_ARGS} ${STAGE0_ARGS}
+  BUILD_ALWAYS ON  # cmake doesn't auto-detect changes without a download method
+  INSTALL_COMMAND ""  # skip install
+  DEPENDS ${EXTRA_DEPENDS}
+)
 ExternalProject_add(stage1
   SOURCE_DIR "${LEAN_SOURCE_DIR}"
   SOURCE_SUBDIR src
   BINARY_DIR stage1
-  CMAKE_ARGS -DSTAGE=1 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage0 -DPREV_STAGE_CMAKE_EXECUTABLE_SUFFIX=${STAGE0_CMAKE_EXECUTABLE_SUFFIX} ${CL_ARGS} ${STAGE1_ARGS}
+  CMAKE_ARGS -DSTAGE=1 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage0 -DPREV_STAGE_CMAKE_EXECUTABLE_SUFFIX=${STAGE0_CMAKE_EXECUTABLE_SUFFIX} ${CL_ARGS}
   BUILD_ALWAYS ON
   INSTALL_COMMAND ""
-  DEPENDS ${EXTRA_DEPENDS}
+  DEPENDS stage0
   STEP_TARGETS configure
 )
 ExternalProject_add(stage2

CMakePresets.json

@@ -24,9 +24,9 @@
     },
     {
       "name": "reldebug",
-      "displayName": "Release with assertions enabled",
+      "displayName": "Release with debug info build config",
       "cacheVariables": {
-        "CMAKE_BUILD_TYPE": "RelWithAssert"
+        "CMAKE_BUILD_TYPE": "RelWithDebInfo"
       },
       "generator": "Unix Makefiles",
       "binaryDir": "${sourceDir}/build/reldebug"

CODEOWNERS

@@ -7,9 +7,8 @@
 /.github/ @kim-em
 /RELEASES.md @kim-em
 /src/kernel/ @leodemoura
-/src/library/compiler/ @zwarich
 /src/lake/ @tydeu
-/src/Lean/Compiler/ @leodemoura @zwarich
+/src/Lean/Compiler/ @leodemoura
 /src/Lean/Data/Lsp/ @mhuisi
 /src/Lean/Elab/Deriving/ @kim-em
 /src/Lean/Elab/Tactic/ @kim-em

doc/dev/release_checklist.md

@@ -144,10 +144,6 @@ We'll use `v4.7.0-rc1` as the intended release version in this example.
     - Run `script/release_steps.py v4.7.0-rc1 <repo>` (e.g. replacing `<repo>` with `batteries`), which will walk you through the following steps:
       - Create a new branch off `master`/`main` (as specified in the `branch` field), called `bump_to_v4.7.0-rc1`.
       - Merge `origin/bump/v4.7.0` if relevant (i.e. `bump-branch: true` appears in `release_repos.yml`).
-      - Otherwise, you *may* need to merge `origin/nightly-testing`.
-      - Note that for `verso` and `reference-manual` development happens on `nightly-testing`, so
-        we will merge that branch into `bump_to_v4.7.0-rc1`, but it is essential in the GitHub interface that we do a rebase merge,
-        in order to preserve the history.
       - Update the contents of `lean-toolchain` to `leanprover/lean4:v4.7.0-rc1`.
       - In the `lakefile.toml` or `lakefile.lean`, if there are dependencies on `nightly-testing`, `bump/v4.7.0`, or specific version tags, update them to the new tag.
         If they depend on `main` or `master`, don't change this; you've just updated the dependency, so `lake update` will take care of modifying the manifest.
@@ -155,7 +151,7 @@ We'll use `v4.7.0-rc1` as the intended release version in this example.
       - Run `lake build && if lake check-test; then lake test; fi` to check things are working.
       - Commit the changes as `chore: bump toolchain to v4.7.0-rc1` and push.
       - Create a PR with title "chore: bump toolchain to v4.7.0-rc1".
-    - Merge the PR once CI completes. (Recall: for `verso` and `reference-manual` you will need to do a rebase merge.)
+    - Merge the PR once CI completes.
     - Re-running `script/release_checklist.py` will then create the tag `v4.7.0-rc1` from `master`/`main` and push it (unless `toolchain-tag: false` in the `release_repos.yml` file)
   - We do this for the same list of repositories as for stable releases, see above for notes about special cases.
     As above, there are dependencies between these, and so the process above is iterative.

flake.lock

@@ -1,50 +1,112 @@
 {
   "nodes": {
-    "nixpkgs": {
+    "flake-utils": {
+      "inputs": {
+        "systems": "systems"
+      },
       "locked": {
-        "lastModified": 1745636243,
-        "narHash": "sha256-kbNvlQZf8wwok3d2X1kM/TlXH/MZ+03ZNv+IPPBx+DM=",
-        "rev": "f771eb401a46846c1aebd20552521b233dd7e18b",
-        "type": "tarball",
-        "url": "https://releases.nixos.org/nixos/unstable/nixos-25.05pre789333.f771eb401a46/nixexprs.tar.xz"
+        "lastModified": 1710146030,
+        "narHash": "sha256-SZ5L6eA7HJ/nmkzGG7/ISclqe6oZdOZTNoesiInkXPQ=",
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "rev": "b1d9ab70662946ef0850d488da1c9019f3a9752a",
+        "type": "github"
       },
       "original": {
-        "type": "tarball",
-        "url": "https://channels.nixos.org/nixos-unstable/nixexprs.tar.xz"
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "type": "github"
+      }
+    },
+    "nixpkgs": {
+      "locked": {
+        "lastModified": 1710889954,
+        "narHash": "sha256-Pr6F5Pmd7JnNEMHHmspZ0qVqIBVxyZ13ik1pJtm2QXk=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "7872526e9c5332274ea5932a0c3270d6e4724f3b",
+        "type": "github"
+      },
+      "original": {
+        "owner": "NixOS",
+        "ref": "nixpkgs-unstable",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "nixpkgs-cadical": {
+      "locked": {
+        "lastModified": 1740791350,
+        "narHash": "sha256-igS2Z4tVw5W/x3lCZeeadt0vcU9fxtetZ/RyrqsCRQ0=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "199169a2135e6b864a888e89a2ace345703c025d",
+        "type": "github"
+      },
+      "original": {
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "199169a2135e6b864a888e89a2ace345703c025d",
+        "type": "github"
       }
     },
     "nixpkgs-old": {
       "flake": false,
       "locked": {
-        "lastModified": 1582018169,
-        "narHash": "sha256-qv1iK1IchpZKSeWL3NEs4U5Jl5QVyNHDdiMJvLOI4Yc=",
-        "type": "tarball",
-        "url": "https://releases.nixos.org/nixos/19.03/nixos-19.03.173691.34c7eb7545d/nixexprs.tar.xz"
+        "lastModified": 1581379743,
+        "narHash": "sha256-i1XCn9rKuLjvCdu2UeXKzGLF6IuQePQKFt4hEKRU5oc=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "34c7eb7545d155cc5b6f499b23a7cb1c96ab4d59",
+        "type": "github"
       },
       "original": {
-        "type": "tarball",
-        "url": "https://channels.nixos.org/nixos-19.03/nixexprs.tar.xz"
+        "owner": "NixOS",
+        "ref": "nixos-19.03",
+        "repo": "nixpkgs",
+        "type": "github"
       }
     },
     "nixpkgs-older": {
       "flake": false,
       "locked": {
-        "lastModified": 1550657948,
-        "narHash": "sha256-BE0XqzNfzvhhtTXv37LyySyq4moL7z1i1hMvwbFNL/I=",
-        "type": "tarball",
-        "url": "https://releases.nixos.org/nixos/18.03/nixos-18.03.133402.cb0e20d6db9/nixexprs.tar.xz"
+        "lastModified": 1523316493,
+        "narHash": "sha256-5qJS+i5ECICPAKA6FhPLIWkhPKDnOZsZbh2PHYF1Kbs=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "0b307aa73804bbd7a7172899e59ae0b8c347a62d",
+        "type": "github"
       },
       "original": {
-        "type": "tarball",
-        "url": "https://channels.nixos.org/nixos-18.03/nixexprs.tar.xz"
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "0b307aa73804bbd7a7172899e59ae0b8c347a62d",
+        "type": "github"
       }
     },
     "root": {
       "inputs": {
+        "flake-utils": "flake-utils",
         "nixpkgs": "nixpkgs",
+        "nixpkgs-cadical": "nixpkgs-cadical",
         "nixpkgs-old": "nixpkgs-old",
         "nixpkgs-older": "nixpkgs-older"
       }
+    },
+    "systems": {
+      "locked": {
+        "lastModified": 1681028828,
+        "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
+        "owner": "nix-systems",
+        "repo": "default",
+        "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nix-systems",
+        "repo": "default",
+        "type": "github"
+      }
     }
   },
   "root": "root",

flake.nix

@@ -1,22 +1,29 @@
 {
   description = "Lean development flake. Not intended for end users.";
 
-  # We use channels so we're not affected by GitHub's rate limits
-  inputs.nixpkgs.url = "https://channels.nixos.org/nixos-unstable/nixexprs.tar.xz";
+  inputs.nixpkgs.url = "github:NixOS/nixpkgs/nixpkgs-unstable";
   # old nixpkgs used for portable release with older glibc (2.27)
-  inputs.nixpkgs-old.url = "https://channels.nixos.org/nixos-19.03/nixexprs.tar.xz";
+  inputs.nixpkgs-old.url = "github:NixOS/nixpkgs/nixos-19.03";
   inputs.nixpkgs-old.flake = false;
   # old nixpkgs used for portable release with older glibc (2.26)
-  inputs.nixpkgs-older.url = "https://channels.nixos.org/nixos-18.03/nixexprs.tar.xz";
+  inputs.nixpkgs-older.url = "github:NixOS/nixpkgs/0b307aa73804bbd7a7172899e59ae0b8c347a62d";
   inputs.nixpkgs-older.flake = false;
+  # for cadical 2.1.2; sync with CMakeLists.txt by taking commit from https://www.nixhub.io/packages/cadical
+  inputs.nixpkgs-cadical.url = "github:NixOS/nixpkgs/199169a2135e6b864a888e89a2ace345703c025d";
+  inputs.flake-utils.url = "github:numtide/flake-utils";
 
-  outputs = inputs: builtins.foldl' inputs.nixpkgs.lib.attrsets.recursiveUpdate {} (builtins.map (system:
+  outputs = inputs: inputs.flake-utils.lib.eachDefaultSystem (system:
     let
       pkgs = import inputs.nixpkgs { inherit system; };
       # An old nixpkgs for creating releases with an old glibc
       pkgsDist-old = import inputs.nixpkgs-older { inherit system; };
       # An old nixpkgs for creating releases with an old glibc
       pkgsDist-old-aarch = import inputs.nixpkgs-old { localSystem.config = "aarch64-unknown-linux-gnu"; };
+      pkgsCadical = import inputs.nixpkgs-cadical { inherit system; };
+      cadical = if pkgs.stdenv.isLinux then
+        # use statically-linked cadical on Linux to avoid glibc versioning troubles
+        pkgsCadical.pkgsStatic.cadical.overrideAttrs { doCheck = false; }
+      else pkgsCadical.cadical;
 
       lean-packages = pkgs.callPackage (./nix/packages.nix) { src = ./.; };
 
@@ -24,7 +31,7 @@
           stdenv = pkgs.overrideCC pkgs.stdenv lean-packages.llvmPackages.clang;
         } ({
           buildInputs = with pkgs; [
-            cmake gmp libuv ccache pkg-config
+            cmake gmp libuv ccache cadical pkg-config
             lean-packages.llvmPackages.llvm  # llvm-symbolizer for asan/lsan
             gdb
             tree  # for CI
@@ -60,17 +67,15 @@
           GDB = pkgsDist.gdb;
         });
     in {
-      packages.${system} = {
+      packages = {
         # to be removed when Nix CI is not needed anymore
         inherit (lean-packages) cacheRoots test update-stage0-commit ciShell;
         deprecated = lean-packages;
       };
 
-      devShells.${system} = {
-        # The default development shell for working on lean itself
-        default = devShellWithDist pkgs;
-        oldGlibc = devShellWithDist pkgsDist-old;
-        oldGlibcAArch = devShellWithDist pkgsDist-old-aarch;
-      };
-    }) ["x86_64-linux" "aarch64-linux"]);
+      # The default development shell for working on lean itself
+      devShells.default = devShellWithDist pkgs;
+      devShells.oldGlibc = devShellWithDist pkgsDist-old;
+      devShells.oldGlibcAArch = devShellWithDist pkgsDist-old-aarch;
+    });
 }

nix/buildLeanPackage.nix

@@ -194,7 +194,7 @@ with builtins; let
   modCandidates = mapAttrs (mod: header:
     let
       deps = if header.errors == []
-             then map (m: m.module) header.result.imports
+             then map (m: m.module) header.imports
              else abort "errors while parsing imports of ${mod}:\n${lib.concatStringsSep "\n" header.errors}";
     in mkMod mod (map (dep: if modDepsMap ? ${dep} then modCandidates.${dep} else externalModMap.${dep}) deps)) modDepsMap;
   expandGlob = g:
@@ -206,7 +206,7 @@ with builtins; let
   # subset of `modCandidates` that is transitively reachable from `roots`
   mods' = listToAttrs (map (e: { name = e.key; value = modCandidates.${e.key}; }) (genericClosure {
     startSet = map (m: { key = m; }) (concatMap expandGlob roots);
-    operator = e: if modDepsMap ? ${e.key} then map (m: { key = m.module; }) (filter (m: modCandidates ? ${m.module}) modDepsMap.${e.key}.result.imports) else [];
+    operator = e: if modDepsMap ? ${e.key} then map (m: { key = m.module; }) (filter (m: modCandidates ? ${m.module}) modDepsMap.${e.key}.imports) else [];
   }));
   allLinkFlags = lib.foldr (shared: acc: acc ++ [ "-L${shared}" "-l${shared.linkName or shared.name}" ]) linkFlags allNativeSharedLibs;
 

script/benchReelabRss.lean

@@ -1,5 +1,4 @@
 import Lean.Data.Lsp
-import Lean.Elab.Import
 open Lean
 open Lean.Lsp
 open Lean.JsonRpc
@@ -8,7 +7,9 @@ open Lean.JsonRpc
 Tests language server memory use by repeatedly re-elaborate a given file.
 
 NOTE: only works on Linux for now.
-ot to touch the imports for usual files.
+
+HACK: The line that is to be prepended with a space is hard-coded below to be sufficiently far down
+not to touch the imports for usual files.
 -/
 
 def main (args : List String) : IO Unit := do
@@ -32,8 +33,6 @@ def main (args : List String) : IO Unit := do
     Ipc.writeRequest ⟨0, "initialize", { capabilities : InitializeParams }⟩
 
     let text ← IO.FS.readFile file
-    let (_, headerEndPos, _) ← Elab.parseImports text
-    let headerEndPos := FileMap.ofString text |>.leanPosToLspPos headerEndPos
     let mut requestNo : Nat := 1
     let mut versionNo : Nat := 1
     Ipc.writeNotification ⟨"textDocument/didOpen", {
@@ -41,14 +40,15 @@ def main (args : List String) : IO Unit := do
     for i in [0:iters.toNat!] do
       if i > 0 then
         versionNo := versionNo + 1
+        let pos := { line := 19, character := 0 }
         let params : DidChangeTextDocumentParams := {
           textDocument := {
             uri      := uri
             version? := versionNo
           }
           contentChanges := #[TextDocumentContentChangeEvent.rangeChange {
-            start := headerEndPos
-            «end» := headerEndPos
+            start := pos
+            «end» := pos
           } " "]
         }
         let params := toJson params

script/merge_remote.py

@@ -47,10 +47,10 @@ def run_command(command, check=True, capture_output=True):
 
 
 def clone_repo(repo, temp_dir):
-    """Clone the repository to a temporary directory."""
-    print(f"Cloning {repo}...")
-    # Remove shallow clone for better merge detection
-    clone_result = run_command(f"gh repo clone {repo} {temp_dir}", check=False)
+    """Clone the repository to a temporary directory using shallow clone."""
+    print(f"Shallow cloning {repo}...")
+    # Keep the shallow clone for efficiency
+    clone_result = run_command(f"gh repo clone {repo} {temp_dir} -- --depth=1", check=False)
     if clone_result.returncode != 0:
         print(f"Failed to clone repository {repo}.")
         print(f"Error: {clone_result.stderr}")
@@ -95,16 +95,26 @@ def check_and_merge(repo, branch, tag, temp_dir):
     if checkout_result.returncode != 0:
         return False
 
-    # Try merging the tag directly
-    print(f"Merging {tag} into {branch}...")
-    merge_result = run_command(f"git merge {tag} --no-edit", check=False)
+    # Try merging the tag in a dry-run to check if it can be merged cleanly
+    print(f"Checking if {tag} can be merged cleanly into {branch}...")
+    merge_check = run_command(f"git merge --no-commit --no-ff {tag}", check=False)
     
-    if merge_result.returncode != 0:
+    if merge_check.returncode != 0:
         print(f"Cannot merge {tag} cleanly into {branch}.")
         print("Merge conflicts would occur. Aborting merge.")
         run_command("git merge --abort")
         return False
     
+    # Abort the test merge
+    run_command("git reset --hard HEAD")
+    
+    # Now perform the actual merge and push to remote
+    print(f"Merging {tag} into {branch}...")
+    merge_result = run_command(f"git merge {tag} --no-edit")
+    if merge_result.returncode != 0:
+        print(f"Failed to merge {tag} into {branch}.")
+        return False
+    
     print(f"Pushing changes to remote...")
     push_result = run_command(f"git push origin {branch}")
     if push_result.returncode != 0:

script/prepare-llvm-linux.sh

@@ -1,5 +1,5 @@
 #!/usr/bin/env bash
-set -euxo pipefail
+set -uo pipefail
 
 # run from root build directory (from inside nix-shell or otherwise defining GLIBC/ZLIB/GMP) as in
 # ```
@@ -14,7 +14,6 @@ set -euxo pipefail
 else
   ln -s llvm llvm-host
 fi
-mkdir -p stage0/lib
 mkdir -p stage1/{bin,lib,lib/glibc,include/clang}
 CP="cp -d"  # preserve symlinks
 # a C compiler!
@@ -26,8 +25,6 @@ cp -L llvm/bin/llvm-ar stage1/bin/
 # dependencies of the above
 $CP llvm/lib/lib{clang-cpp,LLVM}*.so* stage1/lib/
 $CP $ZLIB/lib/libz.so* stage1/lib/
-# also copy USE_LLVM deps into stage 0
-$CP llvm/lib/libLLVM*.so* $ZLIB/lib/libz.so* stage0/lib/
 # general clang++ dependency, breaks cross-library C++ exceptions if linked statically
 $CP $GCC_LIB/lib/libgcc_s.so* stage1/lib/
 # bundle libatomic (referenced by LLVM >= 15, and required by the lean executable to run)
@@ -42,21 +39,20 @@ $CP $GLIBC/lib/*crt* stage1/lib/
 # runtime
 (cd llvm; $CP --parents lib/clang/*/lib/*/{clang_rt.*.o,libclang_rt.builtins*} ../stage1)
 $CP llvm/lib/*/lib{c++,c++abi,unwind}.* $GMP/lib/libgmp.a $LIBUV/lib/libuv.a stage1/lib/
-# LLVM 19 appears to ship the dependencies in 'llvm/lib/<target-triple>/' and 'llvm/include/<target-triple>/'
-# but clang-19 that we use to compile is linked against 'llvm/lib/' and 'llvm/include'
+# LLVM 15 appears to ship the dependencies in 'llvm/lib/<target-triple>/' and 'llvm/include/<target-triple>/'
+# but clang-15 that we use to compile is linked against 'llvm/lib/' and 'llvm/include'
 # https://github.com/llvm/llvm-project/issues/54955
 $CP llvm/lib/*/lib{c++,c++abi,unwind}.* llvm/lib/
 $CP llvm-host/lib/*/lib{c++,c++abi,unwind}.* llvm-host/lib/
 # libc++ headers are looked up in the host compiler's root, so copy over target-specific includes
-$CP -r llvm/include/*-*-* llvm-host/include/ || true
+$CP -r llvm/include/*-*-* llvm-host/include/
 # glibc: use for linking (so Lean programs don't embed newer symbol versions), but not for running (because libc.so, librt.so, and ld.so must be compatible)!
 $CP $GLIBC/lib/libc_nonshared.a stage1/lib/glibc
 # libpthread_nonshared.a must be linked in order to be able to use `pthread_atfork(3)`. LibUV uses this function.
 $CP $GLIBC/lib/libpthread_nonshared.a stage1/lib/glibc
-for f in $GLIBC/lib/{ld,lib{c,dl,m,rt,pthread}}-*; do b=$(basename $f); cp $f stage1/lib/glibc/${b%-*}.so; done
+for f in $GLIBC/lib/lib{c,dl,m,rt,pthread}-*; do b=$(basename $f); cp $f stage1/lib/glibc/${b%-*}.so; done
 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 " -DLEAN_STANDALONE=ON"
 echo -n " -DCMAKE_CXX_COMPILER=$PWD/llvm-host/bin/clang++ -DLEAN_CXX_STDLIB='-Wl,-Bstatic -lc++ -lc++abi -Wl,-Bdynamic'"
 echo -n " -DLEAN_EXTRA_CXX_FLAGS='--sysroot $PWD/llvm -idirafter $GLIBC_DEV/include ${EXTRA_FLAGS:-}'"
 # use target compiler directly when not cross-compiling
@@ -68,9 +64,7 @@ fi
 # use `-nostdinc` to make sure headers are not visible by default (in particular, not to `#include_next` in the clang headers),
 # but do not change sysroot so users can still link against system libs
 echo -n " -DLEANC_INTERNAL_FLAGS='--sysroot ROOT -nostdinc -isystem ROOT/include/clang' -DLEANC_CC=ROOT/bin/clang"
-# ld.so is usually included by the libc.so linker script but we discard those. Make sure it is linked to only after `libc.so` like in the original
-# linker script so that no libc symbols are bound to it instead.
-echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='--sysroot ROOT -L ROOT/lib -L ROOT/lib/glibc -lc -lc_nonshared -Wl,--as-needed -l:ld.so -Wl,--no-as-needed -lpthread_nonshared -Wl,--as-needed -Wl,-Bstatic -lgmp -lunwind -luv -Wl,-Bdynamic -Wl,--no-as-needed -fuse-ld=lld'"
+echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='--sysroot ROOT -L ROOT/lib -L ROOT/lib/glibc ROOT/lib/glibc/libc_nonshared.a ROOT/lib/glibc/libpthread_nonshared.a -Wl,--as-needed -Wl,-Bstatic -lgmp -lunwind -luv -Wl,-Bdynamic -Wl,--no-as-needed -fuse-ld=lld'"
 # when not using the above flags, link GMP dynamically/as usual
 echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-Wl,--as-needed -lgmp -luv -lpthread -ldl -lrt -Wl,--no-as-needed'"
 # do not set `LEAN_CC` for tests

script/release_checklist.py

@@ -7,7 +7,6 @@ import base64
 import subprocess
 import sys
 import os
-import re # Import re module
 # Import run_command from merge_remote.py
 from merge_remote import run_command
 
@@ -59,29 +58,13 @@ def release_page_exists(repo_url, tag_name, github_token):
     response = requests.get(api_url, headers=headers)
     return response.status_code == 200
 
-def get_release_notes(tag_name):
-    """Fetch release notes page title from lean-lang.org."""
-    # Strip -rcX suffix if present for the URL
-    base_tag = tag_name.split('-')[0]
-    reference_url = f"https://lean-lang.org/doc/reference/latest/releases/{base_tag}/"
-    try:
-        response = requests.get(reference_url)
-        response.raise_for_status() # Raise HTTPError for bad responses (4xx or 5xx)
-        
-        # Extract title using regex
-        match = re.search(r"<title>(.*?)</title>", response.text, re.IGNORECASE | re.DOTALL)
-        if match:
-            return match.group(1).strip()
-        else:
-            print(f"  ⚠️ Could not find <title> tag in {reference_url}")
-            return None
-            
-    except requests.exceptions.RequestException as e:
-        print(f"  ❌ Error fetching release notes from {reference_url}: {e}")
-        return None
-    except Exception as e:
-        print(f"  ❌ An unexpected error occurred while processing release notes: {e}")
-        return None
+def get_release_notes(repo_url, tag_name, github_token):
+    api_url = repo_url.replace("https://github.com/", "https://api.github.com/repos/") + f"/releases/tags/{tag_name}"
+    headers = {'Authorization': f'token {github_token}'} if github_token else {}
+    response = requests.get(api_url, headers=headers)
+    if response.status_code == 200:
+        return response.json().get("body", "").strip()
+    return None
 
 def get_branch_content(repo_url, branch, file_path, github_token):
     api_url = repo_url.replace("https://github.com/", "https://api.github.com/repos/") + f"/contents/{file_path}?ref={branch}"
@@ -272,7 +255,6 @@ def main():
     branch_name = f"releases/v{version_major}.{version_minor}.0"
     if not branch_exists(lean_repo_url, branch_name, github_token):
         print(f"  ❌ Branch {branch_name} does not exist")
-        print(f"  🟡 After creating the branch, we'll need to check CMake version settings.")
         lean4_success = False
     else:
         print(f"  ✅ Branch {branch_name} exists")
@@ -292,22 +274,14 @@ def main():
         lean4_success = False
     else:
         print(f"  ✅ Release page for {toolchain} exists")
-        
-    # Check the actual release notes page title
-    actual_title = get_release_notes(toolchain)
-    expected_title_prefix = f"Lean {toolchain.lstrip('v')}" # e.g., "Lean 4.19.0" or "Lean 4.19.0-rc1"
-
-    if actual_title is None:
-        # Error already printed by get_release_notes
-        lean4_success = False
-    elif not actual_title.startswith(expected_title_prefix):
-        # Construct URL for the error message (using the base tag)
-        base_tag = toolchain.split('-')[0]
-        check_url = f"https://lean-lang.org/doc/reference/latest/releases/{base_tag}/"
-        print(f"  ❌ Release notes page title mismatch. Expected prefix '{expected_title_prefix}', got '{actual_title}'. Check {check_url}")
-        lean4_success = False
-    else:
-        print(f"  ✅ Release notes page title looks good ('{actual_title}').")
+        release_notes = get_release_notes(lean_repo_url, toolchain, github_token)
+        if not (release_notes and toolchain in release_notes.splitlines()[0].strip()):
+            previous_minor_version = version_minor - 1
+            previous_release = f"v{version_major}.{previous_minor_version}.0"
+            print(f"  ❌ Release notes not published. Please run `script/release_notes.py --since {previous_release}` on branch `{branch_name}`.")
+            lean4_success = False
+        else:
+            print(f"  ✅ Release notes look good.")
 
     repo_status["lean4"] = lean4_success
 
@@ -386,24 +360,10 @@ def main():
         if check_stable and not is_release_candidate(toolchain):
             if not is_merged_into_stable(url, toolchain, "stable", github_token, verbose):
                 org_repo = extract_org_repo_from_url(url)
-                if args.dry_run:
-                    print(f"  ❌ Tag {toolchain} is not merged into stable")
-                    print(f"     Run `script/merge_remote.py {org_repo} stable {toolchain}` to merge it")
-                    repo_status[name] = False
-                    continue
-                else:
-                    print(f"  … Tag {toolchain} is not merged into stable. Running `script/merge_remote.py {org_repo} stable {toolchain}`...")
-                    
-                    # Run the script to merge the tag
-                    subprocess.run(["script/merge_remote.py", org_repo, "stable", toolchain])
-                    
-                    # Check again if the tag is merged now
-                    if not is_merged_into_stable(url, toolchain, "stable", github_token, verbose):
-                        print(f"  ❌ Manual intervention required.")
-                        repo_status[name] = False
-                        continue
-            
-            # This will print in all successful cases - whether tag was merged initially or was merged successfully
+                print(f"  ❌ Tag {toolchain} is not merged into stable")
+                print(f"     Run `script/merge_remote.py {org_repo} stable {toolchain}` to merge it")
+                repo_status[name] = False
+                continue
             print(f"  ✅ Tag {toolchain} is merged into stable")
 
         if check_bump:

script/release_repos.yml

@@ -21,19 +21,12 @@ repositories:
     branch: master
     dependencies: []
 
-  - name: lean4-cli
-    url: https://github.com/leanprover/lean4-cli
-    toolchain-tag: true
-    stable-branch: false
-    branch: main
-    dependencies: []
-
   - name: doc-gen4
     url: https://github.com/leanprover/doc-gen4
     toolchain-tag: true
     stable-branch: false
     branch: main
-    dependencies: [lean4-cli]
+    dependencies: []
 
   - name: verso
     url: https://github.com/leanprover/verso
@@ -49,13 +42,20 @@ repositories:
     branch: main
     dependencies: [verso]
 
+  - name: lean4-cli
+    url: https://github.com/leanprover/lean4-cli
+    toolchain-tag: true
+    stable-branch: false
+    branch: main
+    dependencies: []
+
   - name: ProofWidgets4
     url: https://github.com/leanprover-community/ProofWidgets4
     toolchain-tag: false
     stable-branch: false
     branch: main
     dependencies:
-      - batteries
+      - Batteries
 
   - name: aesop
     url: https://github.com/leanprover-community/aesop
@@ -63,7 +63,7 @@ repositories:
     stable-branch: true
     branch: master
     dependencies:
-      - batteries
+      - Batteries
 
   - name: import-graph
     url: https://github.com/leanprover-community/import-graph
@@ -71,8 +71,8 @@ repositories:
     stable-branch: false
     branch: main
     dependencies:
-      - lean4-cli
-      - batteries
+      - Cli
+      - Batteries
 
   - name: plausible
     url: https://github.com/leanprover-community/plausible
@@ -88,11 +88,10 @@ repositories:
     branch: master
     bump-branch: true
     dependencies:
-      - aesop
+      - Aesop
       - ProofWidgets4
       - lean4checker
-      - batteries
-      - lean4-cli
+      - Batteries
       - doc-gen4
       - import-graph
       - plausible
@@ -103,4 +102,4 @@ repositories:
     stable-branch: true
     branch: master
     dependencies:
-      - mathlib4
+      - Mathlib

script/release_steps.py

@@ -68,7 +68,7 @@ def generate_script(repo, version, config):
     ]
 
     # Special cases for specific repositories
-    if repo_name == "repl":
+    if repo_name == "REPL":
         script_lines.extend([
             "lake update",
             "cd test/Mathlib",
@@ -79,7 +79,7 @@ def generate_script(repo, version, config):
             "./test.sh"
         ])
     elif dependencies:
-        script_lines.append('perl -pi -e \'s/"v4\\.[0-9]+(\\.[0-9]+)?(-rc[0-9]+)?"/"' + version + '"/g\' lakefile.*')
+        script_lines.append('echo "Please update the dependencies in lakefile.{lean,toml}"')
         script_lines.append("lake update")
 
     script_lines.append("")
@@ -89,20 +89,13 @@ def generate_script(repo, version, config):
         ""
     ])
 
-    if re.search(r'rc\d+$', version) and repo_name in ["batteries", "mathlib4"]:
+    if re.search(r'rc\d+$', version) and repo_name in ["Batteries", "Mathlib"]:
         script_lines.extend([
             "echo 'This repo has nightly-testing infrastructure'",
             f"git merge origin/bump/{version.split('-rc')[0]}",
             "echo 'Please resolve any conflicts.'",
             ""
         ])
-    if re.search(r'rc\d+$', version) and repo_name in ["verso", "reference-manual"]:
-        script_lines.extend([
-            "echo 'This repo does development on nightly-testing: remember to rebase merge the PR.'",
-            f"git merge origin/nightly-testing",
-            "echo 'Please resolve any conflicts.'",
-            ""
-        ])
     if repo_name != "Mathlib":
         script_lines.extend([
             "lake build && if lake check-test; then lake test; fi",
@@ -111,7 +104,7 @@ def generate_script(repo, version, config):
 
     script_lines.extend([
         'gh pr create --title "chore: bump toolchain to ' + version + '" --body ""',
-        "echo 'Please review the PR and merge or rebase it.'",
+        "echo 'Please review the PR and merge it.'",
         ""
     ])
 

src/CMakeLists.txt

@@ -10,7 +10,7 @@ endif()
 include(ExternalProject)
 project(LEAN CXX C)
 set(LEAN_VERSION_MAJOR 4)
-set(LEAN_VERSION_MINOR 21)
+set(LEAN_VERSION_MINOR 20)
 set(LEAN_VERSION_PATCH 0)
 set(LEAN_VERSION_IS_RELEASE 0)  # This number is 1 in the release revision, and 0 otherwise.
 set(LEAN_SPECIAL_VERSION_DESC "" CACHE STRING "Additional version description like 'nightly-2018-03-11'")
@@ -191,11 +191,10 @@ set(CMAKE_MODULE_PATH ${CMAKE_MODULE_PATH} "${CMAKE_SOURCE_DIR}/cmake/Modules")
 
 # Initialize CXXFLAGS.
 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_DEBUG          "-DLEAN_DEBUG -DLEAN_TRACE")
 set(CMAKE_CXX_FLAGS_MINSIZEREL     "-DNDEBUG")
 set(CMAKE_CXX_FLAGS_RELEASE        "-DNDEBUG")
 set(CMAKE_CXX_FLAGS_RELWITHDEBINFO "-DNDEBUG")
-set(CMAKE_CXX_FLAGS_RELWITHASSERT  "-DLEAN_DEBUG")
 
 # SPLIT_STACK
 if (SPLIT_STACK)
@@ -222,7 +221,6 @@ elseif (MSVC)
     set(CMAKE_CXX_FLAGS_DEBUG          "/Od /Zi ${CMAKE_CXX_FLAGS_DEBUG}")
     set(CMAKE_CXX_FLAGS_MINSIZEREL     "/Os /Zc:inline ${CMAKE_CXX_FLAGS_MINSIZEREL}")
     set(CMAKE_CXX_FLAGS_RELEASE        "/O2 /Oi /Oy /Zc:inline ${CMAKE_CXX_FLAGS_RELEASE}")
-    set(CMAKE_CXX_FLAGS_RELWITHASSERT  "/O2 /Oi /Oy /Zc:inline ${CMAKE_CXX_FLAGS_RELWITHASSERT}")
     set(CMAKE_CXX_FLAGS_RELWITHDEBINFO "/O2 /Oi /Zi ${CMAKE_CXX_FLAGS_RELWITHDEBINFO}")
     set(LEAN_EXTRA_LINKER_FLAGS        "/LTCG:INCREMENTAL ${LEAN_EXTRA_LINKER_FLAGS}")
     set(CMAKE_STATIC_LINKER_FLAGS      "${CMAKE_STATIC_LINKER_FLAGS} ${LEAN_EXTRA_LINKER_FLAGS}")
@@ -242,13 +240,11 @@ if (NOT MSVC)
       set(CMAKE_CXX_FLAGS_MINSIZEREL     "-Os ${CMAKE_CXX_FLAGS_MINSIZEREL}")
     endif ()
     set(CMAKE_CXX_FLAGS_RELEASE        "-O3 ${CMAKE_CXX_FLAGS_RELEASE}")
-    set(CMAKE_CXX_FLAGS_RELWITHASSERT  "-O3 ${CMAKE_CXX_FLAGS_RELWITHASSERT}")
     set(CMAKE_CXX_FLAGS_RELWITHDEBINFO "-O2 -g3 -fno-omit-frame-pointer ${CMAKE_CXX_FLAGS_RELWITHDEBINFO}")
 elseif (MULTI_THREAD)
     set(CMAKE_CXX_FLAGS_DEBUG          "/MTd ${CMAKE_CXX_FLAGS_DEBUG}")
     set(CMAKE_CXX_FLAGS_MINSIZEREL     "/MT ${CMAKE_CXX_FLAGS_MINSIZEREL}")
     set(CMAKE_CXX_FLAGS_RELEASE        "/MT ${CMAKE_CXX_FLAGS_RELEASE}")
-    set(CMAKE_CXX_FLAGS_RELWITHASSERT  "/MT ${CMAKE_CXX_FLAGS_RELWITHASSERT}")
     set(CMAKE_CXX_FLAGS_RELWITHDEBINFO "/MT ${CMAKE_CXX_FLAGS_RELWITHDEBINFO}")
 endif ()
 
@@ -369,8 +365,8 @@ if(LLVM)
   execute_process(COMMAND ${LLVM_CONFIG} --version COMMAND_ERROR_IS_FATAL ANY OUTPUT_VARIABLE LLVM_CONFIG_VERSION ECHO_OUTPUT_VARIABLE OUTPUT_STRIP_TRAILING_WHITESPACE)
   string(REGEX MATCH "^[0-9]*" LLVM_CONFIG_MAJOR_VERSION ${LLVM_CONFIG_VERSION})
   message(STATUS "Found 'llvm-config' at '${LLVM_CONFIG}' with version '${LLVM_CONFIG_VERSION}', major version '${LLVM_CONFIG_MAJOR_VERSION}'")
-  if (NOT LLVM_CONFIG_MAJOR_VERSION STREQUAL "19")
-    message(FATAL_ERROR "Unable to find llvm-config version 19. Found invalid version '${LLVM_CONFIG_MAJOR_VERSION}'")
+  if (NOT LLVM_CONFIG_MAJOR_VERSION STREQUAL "15")
+    message(FATAL_ERROR "Unable to find llvm-config version 15. Found invalid version '${LLVM_CONFIG_MAJOR_VERSION}'")
   endif()
   # -DLEAN_LLVM is used to conditionally compile Lean features that depend on LLVM
   string(APPEND CMAKE_CXX_FLAGS " -D LEAN_LLVM")
@@ -511,10 +507,7 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
   # import libraries created by the stdlib.make targets
   string(APPEND LEANC_SHARED_LINKER_FLAGS " -lInit_shared -lleanshared_1 -lleanshared")
 elseif("${CMAKE_SYSTEM_NAME}" MATCHES "Darwin")
-  # The second flag is necessary to even *load* dylibs without resolved symbols, as can happen
-  # if a Lake `extern_lib` depends on a symbols defined by the Lean library but is loaded even
-  # before definition.
-  string(APPEND LEANC_SHARED_LINKER_FLAGS " -Wl,-undefined,dynamic_lookup -Wl,-no_fixup_chains")
+  string(APPEND LEANC_SHARED_LINKER_FLAGS " -Wl,-undefined,dynamic_lookup")
 endif()
 # Linux ignores undefined symbols in shared libraries by default
 
@@ -850,4 +843,6 @@ endif()
 
 if(USE_LAKE AND STAGE EQUAL 1)
   configure_file(${LEAN_SOURCE_DIR}/lakefile.toml.in ${LEAN_SOURCE_DIR}/lakefile.toml)
+  configure_file(${LEAN_SOURCE_DIR}/lakefile.toml.in ${LEAN_SOURCE_DIR}/../tests/lakefile.toml)
+  configure_file(${LEAN_SOURCE_DIR}/lakefile.toml.in ${LEAN_SOURCE_DIR}/../lakefile.toml)
 endif()

src/Init.lean

@@ -3,8 +3,6 @@ Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-module
-
 prelude
 import Init.Prelude
 import Init.Notation

src/Init/BinderNameHint.lean

@@ -4,8 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joachim Breitner
 -/
 
-module
-
 prelude
 import Init.Prelude
 import Init.Tactics

src/Init/BinderPredicates.lean

@@ -3,8 +3,6 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner
 -/
-module
-
 prelude
 import Init.NotationExtra
 

src/Init/ByCases.lean

@@ -3,8 +3,6 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Mario Carneiro
 -/
-module
-
 prelude
 import Init.Classical
 
@@ -42,3 +40,24 @@ theorem apply_ite (f : α → β) (P : Prop) [Decidable P] (x y : α) :
 /-- A `dite` whose results do not actually depend on the condition may be reduced to an `ite`. -/
 @[simp] theorem dite_eq_ite [Decidable P] :
   (dite P (fun _ => a) (fun _ => b)) = ite P a b := rfl
+
+@[deprecated "Use `ite_eq_right_iff`" (since := "2024-09-18")]
+theorem ite_some_none_eq_none [Decidable P] :
+    (if P then some x else none) = none ↔ ¬ P := by
+  simp only [ite_eq_right_iff, reduceCtorEq]
+  rfl
+
+@[deprecated "Use `Option.ite_none_right_eq_some`" (since := "2024-09-18")]
+theorem ite_some_none_eq_some [Decidable P] :
+    (if P then some x else none) = some y ↔ P ∧ x = y := by
+  split <;> simp_all
+
+@[deprecated "Use `dite_eq_right_iff" (since := "2024-09-18")]
+theorem dite_some_none_eq_none [Decidable P] {x : P → α} :
+    (if h : P then some (x h) else none) = none ↔ ¬P := by
+  simp
+
+@[deprecated "Use `Option.dite_none_right_eq_some`" (since := "2024-09-18")]
+theorem dite_some_none_eq_some [Decidable P] {x : P → α} {y : α} :
+    (if h : P then some (x h) else none) = some y ↔ ∃ h : P, x h = y := by
+  by_cases h : P <;> simp [h]

src/Init/Classical.lean

@@ -3,8 +3,6 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Mario Carneiro
 -/
-module
-
 prelude
 import Init.PropLemmas
 

src/Init/Coe.lean

@@ -3,8 +3,6 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Mario Carneiro
 -/
-module
-
 prelude
 import Init.Prelude
 set_option linter.missingDocs true -- keep it documented
@@ -309,6 +307,9 @@ instance boolToSort : CoeSort Bool Prop where
 instance decPropToBool (p : Prop) [Decidable p] : CoeDep Prop p Bool where
   coe := decide p
 
+instance optionCoe {α : Type u} : Coe α (Option α) where
+  coe := some
+
 instance subtypeCoe {α : Sort u} {p : α → Prop} : CoeOut (Subtype p) α where
   coe v := v.val
 

src/Init/Control.lean

@@ -3,8 +3,6 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-module
-
 prelude
 import Init.Control.Basic
 import Init.Control.State

src/Init/Control/Basic.lean

@@ -3,8 +3,6 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura, Sebastian Ullrich
 -/
-module
-
 prelude
 import Init.Core
 import Init.BinderNameHint

src/Init/Control/EState.lean

@@ -3,8 +3,6 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-module
-
 prelude
 import Init.Control.State
 import Init.Control.Except

src/Init/Control/Except.lean

@@ -5,8 +5,6 @@ Authors: Jared Roesch, Sebastian Ullrich
 
 The Except monad transformer.
 -/
-module
-
 prelude
 import Init.Control.Basic
 import Init.Control.Id

src/Init/Control/ExceptCps.lean

@@ -3,8 +3,6 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-module
-
 prelude
 import Init.Control.Lawful.Basic
 

src/Init/Control/Id.lean

@@ -5,8 +5,6 @@ Authors: Sebastian Ullrich
 
 The identity Monad.
 -/
-module
-
 prelude
 import Init.Core
 

src/Init/Control/Lawful.lean

@@ -3,8 +3,6 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Ullrich, Leonardo de Moura, Mario Carneiro
 -/
-module
-
 prelude
 import Init.Control.Lawful.Basic
 import Init.Control.Lawful.Instances

src/Init/Control/Lawful/Basic.lean

@@ -3,8 +3,6 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Ullrich, Leonardo de Moura, Mario Carneiro
 -/
-module
-
 prelude
 import Init.SimpLemmas
 import Init.Meta
@@ -144,7 +142,6 @@ class LawfulMonad (m : Type u → Type v) [Monad m] : Prop extends LawfulApplica
 
 export LawfulMonad (bind_pure_comp bind_map pure_bind bind_assoc)
 attribute [simp] pure_bind bind_assoc bind_pure_comp
-attribute [grind] pure_bind
 
 @[simp] theorem bind_pure [Monad m] [LawfulMonad m] (x : m α) : x >>= pure = x := by
   show x >>= (fun a => pure (id a)) = x

src/Init/Control/Lawful/Instances.lean

@@ -3,8 +3,6 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Ullrich, Leonardo de Moura, Mario Carneiro
 -/
-module
-
 prelude
 import Init.Control.Lawful.Basic
 import Init.Control.Except

src/Init/Control/Lawful/Lemmas.lean

@@ -3,8 +3,6 @@ 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
 import Init.Control.Lawful.Basic
 import Init.RCases

src/Init/Control/Option.lean

@@ -3,8 +3,6 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Sebastian Ullrich
 -/
-module
-
 prelude
 import Init.Data.Option.Basic
 import Init.Control.Basic
@@ -100,7 +98,7 @@ Handles failures by treating them as exceptions of type `Unit`.
 -/
 @[always_inline, inline] protected def tryCatch (x : OptionT m α) (handle : Unit → OptionT m α) : OptionT m α := OptionT.mk do
   let some a ← x | handle ()
-  pure <| some a
+  pure a
 
 instance : MonadExceptOf Unit (OptionT m) where
   throw    := fun _ => OptionT.fail

src/Init/Control/Reader.lean

@@ -5,8 +5,6 @@ Authors: Sebastian Ullrich
 
 The Reader monad transformer for passing immutable State.
 -/
-module
-
 prelude
 import Init.Control.Basic
 import Init.Control.Id

src/Init/Control/State.lean

@@ -5,8 +5,6 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 
 The State monad transformer.
 -/
-module
-
 prelude
 import Init.Control.Basic
 import Init.Control.Id

src/Init/Control/StateCps.lean

@@ -3,8 +3,6 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-module
-
 prelude
 import Init.Control.Lawful.Basic
 

src/Init/Control/StateRef.lean

@@ -5,8 +5,6 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 
 The State monad transformer using IO references.
 -/
-module
-
 prelude
 import Init.System.ST
 

src/Init/Conv.lean

@@ -5,8 +5,6 @@ Authors: Leonardo de Moura
 
 Notation for operators defined at Prelude.lean
 -/
-module
-
 prelude
 import Init.Tactics
 import Init.Meta
@@ -320,25 +318,6 @@ syntax "repeat " convSeq : conv
 macro_rules
   | `(conv| repeat $seq) => `(conv| first | ($seq); repeat $seq | skip)
 
-/--
-Extracts `let` and `let_fun` expressions from within the target expression.
-This is the conv mode version of the `extract_lets` tactic.
-
-- `extract_lets` extracts all the lets from the target.
-- `extract_lets x y z` extracts all the lets from the target and uses `x`, `y`, and `z` for the first names.
-  Using `_` for a name leaves it unnamed.
-
-Limitation: the extracted local declarations do not persist outside of the `conv` goal.
-See also `lift_lets`, which does not extract lets as local declarations.
--/
-syntax (name := extractLets) "extract_lets " optConfig (ppSpace colGt (ident <|> hole))* : conv
-
-/--
-Lifts `let` and `let_fun` expressions within the target expression as far out as possible.
-This is the conv mode version of the `lift_lets` tactic.
--/
-syntax (name := liftLets) "lift_lets " optConfig : conv
-
 /--
 `conv => ...` allows the user to perform targeted rewriting on a goal or hypothesis,
 by focusing on particular subexpressions.

src/Init/Core.lean

@@ -5,8 +5,6 @@ Authors: Leonardo de Moura
 
 notation, basic datatypes and type classes
 -/
-module
-
 prelude
 import Init.Prelude
 import Init.SizeOf
@@ -23,8 +21,6 @@ which applies to all applications of the function).
 
 theorem id_def {α : Sort u} (a : α) : id a = a := rfl
 
-attribute [grind] id
-
 /--
 `flip f a b` is `f b a`. It is useful for "point-free" programming,
 since it can sometimes be used to avoid introducing variables.
@@ -51,9 +47,6 @@ theorem Function.comp_def {α β δ} (f : β → δ) (g : α → β) : f ∘ g =
 @[simp] theorem Function.false_comp {f : α → β} : ((fun _ => false) ∘ f) = fun _ => false := by
   rfl
 
-@[simp] theorem Function.comp_id (f : α → β) : f ∘ id = f := rfl
-@[simp] theorem Function.id_comp (f : α → β) : id ∘ f = f := rfl
-
 attribute [simp] namedPattern
 
 /--
@@ -943,34 +936,6 @@ term.
 theorem eqRec_heq {α : Sort u} {φ : α → Sort v} {a a' : α} : (h : a = a') → (p : φ a) → HEq (Eq.recOn (motive := fun x _ => φ x) h p) p
   | rfl, p => HEq.refl p
 
-/--
-Heterogenous equality with an `Eq.rec` application on the left is equivalent to a heterogenous
-equality on the original term.
--/
-theorem eqRec_heq_iff {α : Sort u} {a : α} {motive : (b : α) → a = b → Sort v}
-    {b : α} {refl : motive a (Eq.refl a)} {h : a = b} {c : motive b h} :
-    HEq (@Eq.rec α a motive refl b h) c ↔ HEq refl c :=
-  h.rec (fun _ => ⟨id, id⟩) c
-
-/--
-Heterogenous equality with an `Eq.rec` application on the right is equivalent to a heterogenous
-equality on the original term.
--/
-theorem heq_eqRec_iff {α : Sort u} {a : α} {motive : (b : α) → a = b → Sort v}
-    {b : α} {refl : motive a (Eq.refl a)} {h : a = b} {c : motive b h} :
-    HEq c (@Eq.rec α a motive refl b h) ↔ HEq c refl :=
-  h.rec (fun _ => ⟨id, id⟩) c
-
-/--
-Moves an cast using `Eq.rec` from the function to the argument.
-Note: because the motive isn't reliably detected by unification,
-it needs to be provided as an explicit parameter.
--/
-theorem apply_eqRec {α : Sort u} {a : α} (motive : (b : α) → a = b → Sort v)
-    {b : α} {h : a = b} {c : motive a (Eq.refl a) → β} {d : motive b h} :
-    @Eq.rec α a (fun b h => motive b h → β) c b h d = c (h.symm ▸ d) := by
-  cases h; rfl
-
 /--
 If casting a term with `Eq.rec` to another type makes it equal to some other term, then the two
 terms are heterogeneously equal.
@@ -1016,7 +981,7 @@ theorem HEq.comm {a : α} {b : β} : HEq a b ↔ HEq b a := Iff.intro HEq.symm H
 theorem heq_comm {a : α} {b : β} : HEq a b ↔ HEq b a := HEq.comm
 
 @[symm] theorem Iff.symm (h : a ↔ b) : b ↔ a := Iff.intro h.mpr h.mp
-theorem Iff.comm : (a ↔ b) ↔ (b ↔ a) := Iff.intro Iff.symm Iff.symm
+theorem Iff.comm: (a ↔ b) ↔ (b ↔ a) := Iff.intro Iff.symm Iff.symm
 theorem iff_comm : (a ↔ b) ↔ (b ↔ a) := Iff.comm
 
 @[symm] theorem And.symm : a ∧ b → b ∧ a := fun ⟨ha, hb⟩ => ⟨hb, ha⟩
@@ -1181,12 +1146,12 @@ theorem dif_eq_if (c : Prop) {h : Decidable c} {α : Sort u} (t : α) (e : α) :
   | isTrue _    => rfl
   | isFalse _   => rfl
 
-instance {c t e : Prop} [dC : Decidable c] [dT : Decidable t] [dE : Decidable e] : Decidable (if c then t else e) :=
+instance {c t e : Prop} [dC : Decidable c] [dT : Decidable t] [dE : Decidable e] : Decidable (if c then t else e)  :=
   match dC with
   | isTrue _   => dT
   | isFalse _  => dE
 
-instance {c : Prop} {t : c → Prop} {e : ¬c → Prop} [dC : Decidable c] [dT : ∀ h, Decidable (t h)] [dE : ∀ h, Decidable (e h)] : Decidable (if h : c then t h else e h) :=
+instance {c : Prop} {t : c → Prop} {e : ¬c → Prop} [dC : Decidable c] [dT : ∀ h, Decidable (t h)] [dE : ∀ h, Decidable (e h)] : Decidable (if h : c then t h else e h)  :=
   match dC with
   | isTrue hc  => dT hc
   | isFalse hc => dE hc
@@ -1902,7 +1867,9 @@ protected abbrev hrecOn
     (f : (a : α) → motive (Quot.mk r a))
     (c : (a b : α) → (p : r a b) → HEq (f a) (f b))
     : motive q :=
-  Quot.recOn q f fun a b p => eq_of_heq (eqRec_heq_iff.mpr (c a b p))
+  Quot.recOn q f fun a b p => eq_of_heq <|
+    have p₁ : HEq (Eq.ndrec (f a) (sound p)) (f a) := eqRec_heq (sound p) (f a)
+    HEq.trans p₁ (c a b p)
 
 end
 end Quot
@@ -2265,27 +2232,6 @@ theorem funext {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x}
   show extfunApp (Quot.mk eqv f) = extfunApp (Quot.mk eqv g)
   exact congrArg extfunApp (Quot.sound h)
 
-/--
-Like `Quot.liftOn q f h` but allows `f a` to "know" that `q = Quot.mk r a`.
--/
-protected abbrev Quot.pliftOn {α : Sort u} {r : α → α → Prop}
-    (q : Quot r)
-    (f : (a : α) → q = Quot.mk r a → β)
-    (h : ∀ (a b : α) (h h'), r a b → f a h = f b h') : β :=
-  q.rec (motive := fun q' => q = q' → β) f
-    (fun a b p => funext fun h' =>
-      (apply_eqRec (motive := fun b _ => q = b)).trans
-        (@h a b (h'.trans (sound p).symm) h' p)) rfl
-
-/--
-Like `Quotient.liftOn q f h` but allows `f a` to "know" that `q = Quotient.mk s a`.
--/
-protected abbrev Quotient.pliftOn {α : Sort u} {s : Setoid α}
-    (q : Quotient s)
-    (f : (a : α) → q = Quotient.mk s a → β)
-    (h : ∀ (a b : α) (h h'), a ≈ b → f a h = f b h') : β :=
-  Quot.pliftOn q f h
-
 instance Pi.instSubsingleton {α : Sort u} {β : α → Sort v} [∀ a, Subsingleton (β a)] :
     Subsingleton (∀ a, β a) where
   allEq f g := funext fun a => Subsingleton.elim (f a) (g a)
@@ -2527,6 +2473,9 @@ class Antisymm (r : α → α → Prop) : Prop where
   /-- An antisymmetric relation `r` satisfies `r a b → r b a → a = b`. -/
   antisymm (a b : α) : r a b → r b a → a = b
 
+@[deprecated Antisymm (since := "2024-10-16"), inherit_doc Antisymm]
+abbrev _root_.Antisymm (r : α → α → Prop) : Prop := Std.Antisymm r
+
 /-- `Asymm X r` means that the binary relation `r` on `X` is asymmetric, that is,
 `r a b → ¬ r b a`. -/
 class Asymm (r : α → α → Prop) : Prop where

src/Init/Data.lean

@@ -3,8 +3,6 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-module
-
 prelude
 import Init.Data.Basic
 import Init.Data.Nat

src/Init/Data/AC.lean

@@ -4,8 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Dany Fabian
 -/
 
-module
-
 prelude
 import Init.Classical
 import Init.ByCases

src/Init/Data/Array.lean

@@ -3,8 +3,6 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner
 -/
-module
-
 prelude
 import Init.Data.Array.Basic
 import Init.Data.Array.QSort

src/Init/Data/Array/Attach.lean

@@ -3,8 +3,6 @@ Copyright (c) 2021 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joachim Breitner, Mario Carneiro
 -/
-module
-
 prelude
 import Init.Data.Array.Mem
 import Init.Data.Array.Lemmas
@@ -56,15 +54,15 @@ well-founded recursion mechanism to prove that the function terminates.
 -/
 @[inline] def attach (xs : Array α) : Array {x // x ∈ xs} := xs.attachWith _ fun _ => id
 
-@[simp, grind =] theorem _root_.List.attachWith_toArray {l : List α} {P : α → Prop} {H : ∀ x ∈ l.toArray, P x} :
+@[simp] theorem _root_.List.attachWith_toArray {l : List α} {P : α → Prop} {H : ∀ x ∈ l.toArray, P x} :
     l.toArray.attachWith P H = (l.attachWith P (by simpa using H)).toArray := by
   simp [attachWith]
 
-@[simp, grind =] theorem _root_.List.attach_toArray {l : List α} :
+@[simp] theorem _root_.List.attach_toArray {l : List α} :
     l.toArray.attach = (l.attachWith (· ∈ l.toArray) (by simp)).toArray := by
   simp [attach]
 
-@[simp, grind =] theorem _root_.List.pmap_toArray {l : List α} {P : α → Prop} {f : ∀ a, P a → β} {H : ∀ a ∈ l.toArray, P a} :
+@[simp] theorem _root_.List.pmap_toArray {l : List α} {P : α → Prop} {f : ∀ a, P a → β} {H : ∀ a ∈ l.toArray, P a} :
     l.toArray.pmap f H = (l.pmap f (by simpa using H)).toArray := by
   simp [pmap]
 
@@ -590,7 +588,7 @@ def unattach {α : Type _} {p : α → Prop} (xs : Array { x // p x }) : Array
   unfold unattach
   simp
 
-@[simp, grind =] theorem _root_.List.unattach_toArray {p : α → Prop} {xs : List { x // p x }} :
+@[simp] theorem _root_.List.unattach_toArray {p : α → Prop} {xs : List { x // p x }} :
     xs.toArray.unattach = xs.unattach.toArray := by
   simp only [unattach, List.map_toArray, List.unattach]
 

src/Init/Data/Array/Basic.lean

@@ -3,8 +3,6 @@ Copyright (c) 2018 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-module
-
 prelude
 import Init.WFTactics
 import Init.Data.Nat.Basic
@@ -36,13 +34,15 @@ variable {α : Type u}
 
 namespace Array
 
+@[deprecated toList (since := "2024-09-10")] abbrev data := @toList
+
 /-! ### Preliminary theorems -/
 
-@[simp, grind] theorem size_set {xs : Array α} {i : Nat} {v : α} (h : i < xs.size) :
+@[simp] theorem size_set {xs : Array α} {i : Nat} {v : α} (h : i < xs.size) :
     (set xs i v h).size = xs.size :=
   List.length_set ..
 
-@[simp, grind] theorem size_push {xs : Array α} (v : α) : (push xs v).size = xs.size + 1 :=
+@[simp] theorem size_push {xs : Array α} (v : α) : (push xs v).size = xs.size + 1 :=
   List.length_concat ..
 
 theorem ext {xs ys : Array α}
@@ -86,11 +86,11 @@ theorem ext' {xs ys : Array α} (h : xs.toList = ys.toList) : xs = ys := by
 @[simp] theorem toArrayAux_eq {as : List α} {acc : Array α} : (as.toArrayAux acc).toList = acc.toList ++ as := by
   induction as generalizing acc <;> simp [*, List.toArrayAux, Array.push, List.append_assoc, List.concat_eq_append]
 
-@[simp, grind =] theorem toArray_toList {xs : Array α} : xs.toList.toArray = xs := rfl
+@[simp] theorem toArray_toList {xs : Array α} : xs.toList.toArray = xs := rfl
 
-@[simp, grind =] theorem getElem_toList {xs : Array α} {i : Nat} (h : i < xs.size) : xs.toList[i] = xs[i] := rfl
+@[simp] theorem getElem_toList {xs : Array α} {i : Nat} (h : i < xs.size) : xs.toList[i] = xs[i] := rfl
 
-@[simp, grind =] theorem getElem?_toList {xs : Array α} {i : Nat} : xs.toList[i]? = xs[i]? := by
+@[simp] theorem getElem?_toList {xs : Array α} {i : Nat} : xs.toList[i]? = xs[i]? := by
   simp [getElem?_def]
 
 /-- `a ∈ as` is a predicate which asserts that `a` is in the array `as`. -/
@@ -105,10 +105,10 @@ instance : Membership α (Array α) where
 theorem mem_def {a : α} {as : Array α} : a ∈ as ↔ a ∈ as.toList :=
   ⟨fun | .mk h => h, Array.Mem.mk⟩
 
-@[simp, grind =] theorem mem_toArray {a : α} {l : List α} : a ∈ l.toArray ↔ a ∈ l := by
+@[simp] theorem mem_toArray {a : α} {l : List α} : a ∈ l.toArray ↔ a ∈ l := by
   simp [mem_def]
 
-@[simp, grind] theorem getElem_mem {xs : Array α} {i : Nat} (h : i < xs.size) : xs[i] ∈ xs := by
+@[simp] theorem getElem_mem {xs : Array α} {i : Nat} (h : i < xs.size) : xs[i] ∈ xs := by
   rw [Array.mem_def, ← getElem_toList]
   apply List.getElem_mem
 
@@ -125,18 +125,18 @@ theorem toList_toArray {as : List α} : as.toArray.toList = as := rfl
 @[deprecated toList_toArray (since := "2025-02-17")]
 abbrev _root_.Array.toList_toArray := @List.toList_toArray
 
-@[simp, grind] theorem size_toArray {as : List α} : as.toArray.size = as.length := by simp [Array.size]
+@[simp] theorem size_toArray {as : List α} : as.toArray.size = as.length := by simp [Array.size]
 
 @[deprecated size_toArray (since := "2025-02-17")]
 abbrev _root_.Array.size_toArray := @List.size_toArray
 
-@[simp, grind =] theorem getElem_toArray {xs : List α} {i : Nat} (h : i < xs.toArray.size) :
+@[simp] theorem getElem_toArray {xs : List α} {i : Nat} (h : i < xs.toArray.size) :
     xs.toArray[i] = xs[i]'(by simpa using h) := rfl
 
-@[simp, grind =] theorem getElem?_toArray {xs : List α} {i : Nat} : xs.toArray[i]? = xs[i]? := by
+@[simp] theorem getElem?_toArray {xs : List α} {i : Nat} : xs.toArray[i]? = xs[i]? := by
   simp [getElem?_def]
 
-@[simp, grind =] theorem getElem!_toArray [Inhabited α] {xs : List α} {i : Nat} :
+@[simp] theorem getElem!_toArray [Inhabited α] {xs : List α} {i : Nat} :
     xs.toArray[i]! = xs[i]! := by
   simp [getElem!_def]
 
@@ -146,6 +146,8 @@ namespace Array
 
 theorem size_eq_length_toList {xs : Array α} : xs.size = xs.toList.length := rfl
 
+@[deprecated toList_toArray (since := "2024-09-09")] abbrev data_toArray := @List.toList_toArray
+
 /-! ### Externs -/
 
 /--
@@ -190,7 +192,7 @@ Examples:
 def pop (xs : Array α) : Array α where
   toList := xs.toList.dropLast
 
-@[simp, grind] theorem size_pop {xs : Array α} : xs.pop.size = xs.size - 1 := by
+@[simp] theorem size_pop {xs : Array α} : xs.pop.size = xs.size - 1 := by
   match xs with
   | ⟨[]⟩ => rfl
   | ⟨a::as⟩ => simp [pop, Nat.succ_sub_succ_eq_sub, size]
@@ -832,7 +834,7 @@ some 10
 def findSomeM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m (Option β)) (as : Array α) : m (Option β) := do
   for a in as do
     match (← f a) with
-    | some b => return some b
+    | some b => return b
     | _      => pure ⟨⟩
   return none
 
@@ -863,7 +865,7 @@ some 1
 def findM? {α : Type} [Monad m] (p : α → m Bool) (as : Array α) : m (Option α) := do
   for a in as do
     if (← p a) then
-      return some a
+      return a
   return none
 
 /--
@@ -1171,7 +1173,7 @@ def find? {α : Type u} (p : α → Bool) (as : Array α) : Option α :=
   Id.run do
     for a in as do
       if p a then
-        return some a
+        return a
     return none
 
 /--
@@ -1483,6 +1485,8 @@ The resulting arrays are appended.
 def flatMapM [Monad m] (f : α → m (Array β)) (as : Array α) : m (Array β) :=
   as.foldlM (init := empty) fun bs a => do return bs ++ (← f a)
 
+@[deprecated flatMapM (since := "2024-10-16")] abbrev concatMapM := @flatMapM
+
 /--
 Applies a function that returns an array to each element of an array. The resulting arrays are
 appended.
@@ -1495,6 +1499,8 @@ Examples:
 def flatMap (f : α → Array β) (as : Array α) : Array β :=
   as.foldl (init := empty) fun bs a => bs ++ f a
 
+@[deprecated flatMap (since := "2024-10-16")] abbrev concatMap := @flatMap
+
 /--
 Appends the contents of array of arrays into a single array. The resulting array contains the same
 elements as the nested arrays in the same order.
@@ -2150,15 +2156,13 @@ Examples:
 
 /-! ### Repr and ToString -/
 
-protected def Array.repr {α : Type u} [Repr α] (xs : Array α) : Std.Format :=
-  let _ : Std.ToFormat α := ⟨repr⟩
-  if xs.size == 0 then
-    "#[]"
-  else
-    Std.Format.bracketFill "#[" (Std.Format.joinSep (toList xs) ("," ++ Std.Format.line)) "]"
-
 instance {α : Type u} [Repr α] : Repr (Array α) where
-  reprPrec xs _ := Array.repr xs
+  reprPrec xs _ :=
+    let _ : Std.ToFormat α := ⟨repr⟩
+    if xs.size == 0 then
+      "#[]"
+    else
+      Std.Format.bracketFill "#[" (Std.Format.joinSep (toList xs) ("," ++ Std.Format.line)) "]"
 
 instance [ToString α] : ToString (Array α) where
   toString xs := "#" ++ toString xs.toList

src/Init/Data/Array/BasicAux.lean

@@ -3,8 +3,6 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-module
-
 prelude
 import Init.Data.Array.Basic
 import Init.Data.Nat.Linear

src/Init/Data/Array/BinSearch.lean

@@ -3,8 +3,6 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-module
-
 prelude
 import Init.Data.Array.Basic
 import Init.Data.Int.DivMod.Lemmas

src/Init/Data/Array/Bootstrap.lean

@@ -4,8 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 
-module
-
 prelude
 import Init.Data.List.TakeDrop
 
@@ -55,12 +53,12 @@ theorem foldlM_toList.aux [Monad m]
     rfl
   · rw [List.drop_of_length_le (Nat.ge_of_not_lt ‹_›)]; rfl
 
-@[simp, grind =] theorem foldlM_toList [Monad m]
+@[simp] theorem foldlM_toList [Monad m]
     {f : β → α → m β} {init : β} {xs : Array α} :
     xs.toList.foldlM f init = xs.foldlM f init := by
   simp [foldlM, foldlM_toList.aux]
 
-@[simp, grind =] theorem foldl_toList (f : β → α → β) {init : β} {xs : Array α} :
+@[simp] theorem foldl_toList (f : β → α → β) {init : β} {xs : Array α} :
     xs.toList.foldl f init = xs.foldl f init :=
   List.foldl_eq_foldlM .. ▸ foldlM_toList ..
 
@@ -79,32 +77,32 @@ theorem foldrM_eq_reverse_foldlM_toList [Monad m] {f : α → β → m β} {init
   match xs, this with | _, .inl rfl => rfl | xs, .inr h => ?_
   simp [foldrM, h, ← foldrM_eq_reverse_foldlM_toList.aux, List.take_length]
 
-@[simp, grind =] theorem foldrM_toList [Monad m]
+@[simp] theorem foldrM_toList [Monad m]
     {f : α → β → m β} {init : β} {xs : Array α} :
     xs.toList.foldrM f init = xs.foldrM f init := by
   rw [foldrM_eq_reverse_foldlM_toList, List.foldlM_reverse]
 
-@[simp, grind =] theorem foldr_toList (f : α → β → β) {init : β} {xs : Array α} :
+@[simp] theorem foldr_toList (f : α → β → β) {init : β} {xs : Array α} :
     xs.toList.foldr f init = xs.foldr f init :=
   List.foldr_eq_foldrM .. ▸ foldrM_toList ..
 
-@[simp, grind =] theorem push_toList {xs : Array α} {a : α} : (xs.push a).toList = xs.toList ++ [a] := by
+@[simp] theorem push_toList {xs : Array α} {a : α} : (xs.push a).toList = xs.toList ++ [a] := by
   simp [push, List.concat_eq_append]
 
-@[simp, grind =] theorem toListAppend_eq {xs : Array α} {l : List α} : xs.toListAppend l = xs.toList ++ l := by
+@[simp] theorem toListAppend_eq {xs : Array α} {l : List α} : xs.toListAppend l = xs.toList ++ l := by
   simp [toListAppend, ← foldr_toList]
 
-@[simp, grind =] theorem toListImpl_eq {xs : Array α} : xs.toListImpl = xs.toList := by
+@[simp] theorem toListImpl_eq {xs : Array α} : xs.toListImpl = xs.toList := by
   simp [toListImpl, ← foldr_toList]
 
-@[simp, grind =] theorem toList_pop {xs : Array α} : xs.pop.toList = xs.toList.dropLast := rfl
+@[simp] theorem toList_pop {xs : Array α} : xs.pop.toList = xs.toList.dropLast := rfl
 
 @[deprecated toList_pop (since := "2025-02-17")]
 abbrev pop_toList := @Array.toList_pop
 
 @[simp] theorem append_eq_append {xs ys : Array α} : xs.append ys = xs ++ ys := rfl
 
-@[simp, grind =] theorem toList_append {xs ys : Array α} :
+@[simp] theorem toList_append {xs ys : Array α} :
     (xs ++ ys).toList = xs.toList ++ ys.toList := by
   rw [← append_eq_append]; unfold Array.append
   rw [← foldl_toList]
@@ -112,24 +110,24 @@ abbrev pop_toList := @Array.toList_pop
 
 @[simp] theorem toList_empty : (#[] : Array α).toList = [] := rfl
 
-@[simp, grind =] theorem append_empty {xs : Array α} : xs ++ #[] = xs := by
+@[simp] theorem append_empty {xs : Array α} : xs ++ #[] = xs := by
   apply ext'; simp only [toList_append, toList_empty, List.append_nil]
 
 @[deprecated append_empty (since := "2025-01-13")]
 abbrev append_nil := @append_empty
 
-@[simp, grind =] theorem empty_append {xs : Array α} : #[] ++ xs = xs := by
+@[simp] theorem empty_append {xs : Array α} : #[] ++ xs = xs := by
   apply ext'; simp only [toList_append, toList_empty, List.nil_append]
 
 @[deprecated empty_append (since := "2025-01-13")]
 abbrev nil_append := @empty_append
 
-@[simp, grind _=_] theorem append_assoc {xs ys zs : Array α} : xs ++ ys ++ zs = xs ++ (ys ++ zs) := by
+@[simp] theorem append_assoc {xs ys zs : Array α} : xs ++ ys ++ zs = xs ++ (ys ++ zs) := by
   apply ext'; simp only [toList_append, List.append_assoc]
 
 @[simp] theorem appendList_eq_append {xs : Array α} {l : List α} : xs.appendList l = xs ++ l := rfl
 
-@[simp, grind =] theorem toList_appendList {xs : Array α} {l : List α} :
+@[simp] theorem toList_appendList {xs : Array α} {l : List α} :
     (xs ++ l).toList = xs.toList ++ l := by
   rw [← appendList_eq_append]; unfold Array.appendList
   induction l generalizing xs <;> simp [*]
@@ -159,4 +157,34 @@ theorem foldl_eq_foldl_toList {f : β → α → β} {init : β} {xs : Array α}
     xs.foldl f init = xs.toList.foldl f init:= by
   simp
 
+@[deprecated foldlM_toList (since := "2024-09-09")]
+abbrev foldlM_eq_foldlM_data := @foldlM_toList
+
+@[deprecated foldl_toList (since := "2024-09-09")]
+abbrev foldl_eq_foldl_data := @foldl_toList
+
+@[deprecated foldrM_eq_reverse_foldlM_toList (since := "2024-09-09")]
+abbrev foldrM_eq_reverse_foldlM_data := @foldrM_eq_reverse_foldlM_toList
+
+@[deprecated foldrM_toList (since := "2024-09-09")]
+abbrev foldrM_eq_foldrM_data := @foldrM_toList
+
+@[deprecated foldr_toList (since := "2024-09-09")]
+abbrev foldr_eq_foldr_data := @foldr_toList
+
+@[deprecated push_toList (since := "2024-09-09")]
+abbrev push_data := @push_toList
+
+@[deprecated toListImpl_eq (since := "2024-09-09")]
+abbrev toList_eq := @toListImpl_eq
+
+@[deprecated pop_toList (since := "2024-09-09")]
+abbrev pop_data := @toList_pop
+
+@[deprecated toList_append (since := "2024-09-09")]
+abbrev append_data := @toList_append
+
+@[deprecated toList_appendList (since := "2024-09-09")]
+abbrev appendList_data := @toList_appendList
+
 end Array

src/Init/Data/Array/Count.lean

@@ -3,8 +3,6 @@ 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
 import Init.Data.Array.Lemmas
 import Init.Data.List.Nat.Count
@@ -25,7 +23,7 @@ section countP
 
 variable {p q : α → Bool}
 
-@[simp, grind =] theorem _root_.List.countP_toArray {l : List α} : countP p l.toArray = l.countP p := by
+@[simp] theorem _root_.List.countP_toArray {l : List α} : countP p l.toArray = l.countP p := by
   simp [countP]
   induction l with
   | nil => rfl
@@ -33,7 +31,7 @@ variable {p q : α → Bool}
     simp only [List.foldr_cons, ih, List.countP_cons]
     split <;> simp_all
 
-@[simp, grind =] theorem countP_toList {xs : Array α} : xs.toList.countP p = countP p xs := by
+@[simp] theorem countP_toList {xs : Array α} : xs.toList.countP p = countP p xs := by
   cases xs
   simp
 
@@ -164,10 +162,10 @@ section count
 
 variable [BEq α]
 
-@[simp, grind =] theorem _root_.List.count_toArray {l : List α} {a : α} : count a l.toArray = l.count a := by
+@[simp] theorem _root_.List.count_toArray {l : List α} {a : α} : count a l.toArray = l.count a := by
   simp [count, List.count_eq_countP]
 
-@[simp, grind =] theorem count_toList {xs : Array α} {a : α} : xs.toList.count a = xs.count a := by
+@[simp] theorem count_toList {xs : Array α} {a : α} : xs.toList.count a = xs.count a := by
   cases xs
   simp
 

src/Init/Data/Array/DecidableEq.lean

@@ -3,8 +3,6 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-module
-
 prelude
 import Init.Data.Array.Basic
 import Init.Data.BEq
@@ -68,7 +66,7 @@ theorem isEqv_eq_decide (xs ys : Array α) (r) :
       Bool.not_eq_true]
     simpa [isEqv_iff_rel] using h'
 
-@[simp, grind =] theorem isEqv_toList [BEq α] (xs ys : Array α) : (xs.toList.isEqv ys.toList r) = (xs.isEqv ys r) := by
+@[simp] theorem isEqv_toList [BEq α] (xs ys : Array α) : (xs.toList.isEqv ys.toList r) = (xs.isEqv ys r) := by
   simp [isEqv_eq_decide, List.isEqv_eq_decide]
 
 theorem eq_of_isEqv [DecidableEq α] (xs ys : Array α) (h : Array.isEqv xs ys (fun x y => x = y)) : xs = ys := by
@@ -99,17 +97,17 @@ theorem beq_eq_decide [BEq α] (xs ys : Array α) :
       decide (∀ (i : Nat) (h' : i < xs.size), xs[i] == ys[i]'(h ▸ h')) else false := by
   simp [BEq.beq, isEqv_eq_decide]
 
-@[simp, grind =] theorem beq_toList [BEq α] (xs ys : Array α) : (xs.toList == ys.toList) = (xs == ys) := by
+@[simp] theorem beq_toList [BEq α] (xs ys : Array α) : (xs.toList == ys.toList) = (xs == ys) := by
   simp [beq_eq_decide, List.beq_eq_decide]
 
 end Array
 
 namespace List
 
-@[simp, grind =] theorem isEqv_toArray [BEq α] (as bs : List α) : (as.toArray.isEqv bs.toArray r) = (as.isEqv bs r) := by
+@[simp] theorem isEqv_toArray [BEq α] (as bs : List α) : (as.toArray.isEqv bs.toArray r) = (as.isEqv bs r) := by
   simp [isEqv_eq_decide, Array.isEqv_eq_decide]
 
-@[simp, grind =] theorem beq_toArray [BEq α] (as bs : List α) : (as.toArray == bs.toArray) = (as == bs) := by
+@[simp] theorem beq_toArray [BEq α] (as bs : List α) : (as.toArray == bs.toArray) = (as == bs) := by
   simp [beq_eq_decide, Array.beq_eq_decide]
 
 end List

src/Init/Data/Array/Erase.lean

@@ -3,8 +3,6 @@ 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
 import Init.Data.Array.Lemmas
 import Init.Data.List.Nat.Erase

src/Init/Data/Array/Extract.lean

@@ -3,8 +3,6 @@ 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
 import Init.Data.Array.Lemmas
 import Init.Data.List.Nat.TakeDrop

src/Init/Data/Array/FinRange.lean

@@ -3,8 +3,6 @@ Copyright (c) 2024 François G. Dorais. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: François G. Dorais
 -/
-module
-
 prelude
 import Init.Data.List.FinRange
 import Init.Data.Array.OfFn

src/Init/Data/Array/Find.lean

@@ -3,8 +3,6 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
-module
-
 prelude
 import Init.Data.List.Nat.Find
 import Init.Data.Array.Lemmas
@@ -23,14 +21,6 @@ open Nat
 
 /-! ### findSome? -/
 
-@[simp, grind] theorem findSome?_empty : (#[] : Array α).findSome? f = none := rfl
-@[simp, grind] theorem findSome?_push {xs : Array α} : (xs.push a).findSome? f = (xs.findSome? f).or (f a) := by
-  cases xs; simp [List.findSome?_append]
-
-@[grind]
-theorem findSome?_singleton {a : α} {f : α → Option β} : #[a].findSome? f = f a := by
-  simp
-
 @[simp] theorem findSomeRev?_push_of_isSome {xs : Array α} (h : (f a).isSome) : (xs.push a).findSomeRev? f = f a := by
   cases xs; simp_all
 
@@ -38,7 +28,7 @@ theorem findSome?_singleton {a : α} {f : α → Option β} : #[a].findSome? f =
   cases xs; simp_all
 
 theorem exists_of_findSome?_eq_some {f : α → Option β} {xs : Array α} (w : xs.findSome? f = some b) :
-    ∃ a, a ∈ xs ∧ f a = some b := by
+    ∃ a, a ∈ xs ∧ f a = b := by
   cases xs; simp_all [List.exists_of_findSome?_eq_some]
 
 @[simp] theorem findSome?_eq_none_iff : findSome? p xs = none ↔ ∀ x ∈ xs, p x = none := by
@@ -139,8 +129,6 @@ abbrev findSome?_mkArray_of_isNone := @findSome?_replicate_of_isNone
 
 /-! ### find? -/
 
-@[simp] theorem find?_empty : find? p #[] = none := rfl
-
 @[simp] theorem find?_singleton {a : α} {p : α → Bool} :
     #[a].find? p = if p a then some a else none := by
   simp [singleton_eq_toArray_singleton]
@@ -169,9 +157,6 @@ theorem find?_eq_some_iff_append {xs : Array α} :
     exact ⟨as.toList, ⟨l, by simpa using congrArg Array.toList h'⟩,
       by simpa using h⟩
 
-theorem find?_push {xs : Array α} : (xs.push a).find? p = (xs.find? p).or (if p a then some a else none) := by
-  cases xs; simp
-
 @[simp]
 theorem find?_push_eq_some {xs : Array α} :
     (xs.push a).find? p = some b ↔ xs.find? p = some b ∨ (xs.find? p = none ∧ (p a ∧ a = b)) := by
@@ -346,11 +331,6 @@ theorem find?_eq_some_iff_getElem {xs : Array α} {p : α → Bool} {b : α} :
 
 /-! ### findIdx -/
 
-@[simp] theorem findIdx_empty : findIdx p #[] = 0 := rfl
-theorem findIdx_singleton {a : α} {p : α → Bool} :
-    #[a].findIdx p = if p a then 0 else 1 := by
-  simp
-
 theorem findIdx_of_getElem?_eq_some {xs : Array α} (w : xs[xs.findIdx p]? = some y) : p y := by
   rcases xs with ⟨xs⟩
   exact List.findIdx_of_getElem?_eq_some (by simpa using w)
@@ -431,13 +411,6 @@ theorem findIdx_append {p : α → Bool} {xs ys : Array α} :
   rcases ys with ⟨ys⟩
   simp [List.findIdx_append]
 
-theorem findIdx_push {xs : Array α} {a : α} {p : α → Bool} :
-    (xs.push a).findIdx p = if xs.findIdx p < xs.size then xs.findIdx p else xs.size + if p a then 0 else 1 := by
-  simp only [push_eq_append, findIdx_append]
-  split <;> rename_i h
-  · rfl
-  · simp [findIdx_singleton, Nat.add_comm]
-
 theorem findIdx_le_findIdx {xs : Array α} {p q : α → Bool} (h : ∀ x ∈ xs, p x → q x) : xs.findIdx q ≤ xs.findIdx p := by
   rcases xs with ⟨xs⟩
   simp_all [List.findIdx_le_findIdx]
@@ -466,9 +439,6 @@ theorem false_of_mem_extract_findIdx {xs : Array α} {p : α → Bool} (h : x
 /-! ### findIdx? -/
 
 @[simp] theorem findIdx?_empty : (#[] : Array α).findIdx? p = none := by simp
-theorem findIdx?_singleton {a : α} {p : α → Bool} :
-    #[a].findIdx? p = if p a then some 0 else none := by
-  simp
 
 @[simp]
 theorem findIdx?_eq_none_iff {xs : Array α} {p : α → Bool} :
@@ -536,13 +506,6 @@ theorem of_findIdx?_eq_none {xs : Array α} {p : α → Bool} (w : xs.findIdx? p
   rcases ys with ⟨ys⟩
   simp [List.findIdx?_append]
 
-theorem findIdx?_push {xs : Array α} {a : α} {p : α → Bool} :
-    (xs.push a).findIdx? p = (xs.findIdx? p).or (if p a then some xs.size else none) := by
-  simp only [push_eq_append, findIdx?_append]
-  split <;> rename_i h
-  · simp only [findIdx?_singleton, if_pos h, Option.map_some, Nat.zero_add]
-  · simp only [findIdx?_singleton, if_neg h, Option.map_none]
-
 theorem findIdx?_flatten {xss : Array (Array α)} {p : α → Bool} :
     xss.flatten.findIdx? p =
       (xss.findIdx? (·.any p)).map
@@ -600,9 +563,6 @@ theorem findIdx?_eq_some_le_of_findIdx?_eq_some {xs : Array α} {p q : α → Bo
 /-! ### findFinIdx? -/
 
 @[simp] theorem findFinIdx?_empty {p : α → Bool} : findFinIdx? p #[] = none := by simp
-theorem findFinIdx?_singleton {a : α} {p : α → Bool} :
-    #[a].findFinIdx? p = if p a then some ⟨0, by simp⟩ else none := by
-  simp
 
 -- We can't mark this as a `@[congr]` lemma since the head of the RHS is not `findFinIdx?`.
 theorem findFinIdx?_congr {p : α → Bool} {xs ys : Array α} (w : xs = ys) :
@@ -633,21 +593,6 @@ theorem findFinIdx?_eq_some_iff {xs : Array α} {p : α → Bool} {i : Fin xs.si
   · rintro ⟨h, w⟩
     exact ⟨i, ⟨i.2, h, fun j hji => w ⟨j, by omega⟩ hji⟩, rfl⟩
 
-theorem findFinIdx?_push {xs : Array α} {a : α} {p : α → Bool} :
-    (xs.push a).findFinIdx? p =
-      ((xs.findFinIdx? p).map (Fin.castLE (by simp))).or (if p a then some ⟨xs.size, by simp⟩ else none) := by
-  simp only [findFinIdx?_eq_pmap_findIdx?, findIdx?_push, Option.pmap_or]
-  split <;> rename_i h _ <;> split <;> simp [h]
-
-theorem findFinIdx?_append {xs ys : Array α} {p : α → Bool} :
-    (xs ++ ys).findFinIdx? p =
-      ((xs.findFinIdx? p).map (Fin.castLE (by simp))).or
-        ((ys.findFinIdx? p).map (Fin.natAdd xs.size) |>.map (Fin.cast (by simp))) := by
-  simp only [findFinIdx?_eq_pmap_findIdx?, findIdx?_append, Option.pmap_or]
-  split <;> rename_i h _
-  · simp [h, Option.pmap_map, Option.map_pmap, Nat.add_comm]
-  · simp [h]
-
 @[simp]
 theorem isSome_findFinIdx? {xs : Array α} {p : α → Bool} :
     (xs.findFinIdx? p).isSome = xs.any p := by

src/Init/Data/Array/GetLit.lean

@@ -4,8 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 
-module
-
 prelude
 import Init.Data.Array.Basic
 

src/Init/Data/Array/InsertIdx.lean

@@ -3,8 +3,6 @@ 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
 import Init.Data.Array.Lemmas
 import Init.Data.List.Nat.InsertIdx

src/Init/Data/Array/InsertionSort.lean

@@ -3,8 +3,6 @@ Copyright (c) 2018 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-module
-
 prelude
 import Init.Data.Array.Basic
 

src/Init/Data/Array/Lex.lean

@@ -3,8 +3,6 @@ Copyright (c) 2024 Lean FRO. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Kim Morrison
 -/
-module
-
 prelude
 import Init.Data.Array.Lex.Basic
 import Init.Data.Array.Lex.Lemmas

src/Init/Data/Array/Lex/Basic.lean

@@ -3,8 +3,6 @@ Copyright (c) 2024 Lean FRO. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Kim Morrison
 -/
-module
-
 prelude
 import Init.Data.Array.Basic
 import Init.Data.Nat.Lemmas

src/Init/Data/Array/Lex/Lemmas.lean

@@ -3,8 +3,6 @@ Copyright (c) 2024 Lean FRO. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Kim Morrison
 -/
-module
-
 prelude
 import Init.Data.Array.Lemmas
 import Init.Data.List.Lex
@@ -16,11 +14,11 @@ namespace Array
 
 /-! ### Lexicographic ordering -/
 
-@[simp, grind =] theorem _root_.List.lt_toArray [LT α] {l₁ l₂ : List α} : l₁.toArray < l₂.toArray ↔ l₁ < l₂ := Iff.rfl
-@[simp, grind =] theorem _root_.List.le_toArray [LT α] {l₁ l₂ : List α} : l₁.toArray ≤ l₂.toArray ↔ l₁ ≤ l₂ := Iff.rfl
+@[simp] theorem _root_.List.lt_toArray [LT α] {l₁ l₂ : List α} : l₁.toArray < l₂.toArray ↔ l₁ < l₂ := Iff.rfl
+@[simp] theorem _root_.List.le_toArray [LT α] {l₁ l₂ : List α} : l₁.toArray ≤ l₂.toArray ↔ l₁ ≤ l₂ := Iff.rfl
 
-@[simp, grind =] theorem lt_toList [LT α] {xs ys : Array α} : xs.toList < ys.toList ↔ xs < ys := Iff.rfl
-@[simp, grind =] theorem le_toList [LT α] {xs ys : Array α} : xs.toList ≤ ys.toList ↔ xs ≤ ys := Iff.rfl
+@[simp] theorem lt_toList [LT α] {xs ys : Array α} : xs.toList < ys.toList ↔ xs < ys := Iff.rfl
+@[simp] theorem le_toList [LT α] {xs ys : Array α} : xs.toList ≤ ys.toList ↔ xs ≤ ys := Iff.rfl
 
 protected theorem not_lt_iff_ge [LT α] {l₁ l₂ : List α} : ¬ l₁ < l₂ ↔ l₂ ≤ l₁ := Iff.rfl
 protected theorem not_le_iff_gt [DecidableEq α] [LT α] [DecidableLT α] {l₁ l₂ : List α} :
@@ -47,7 +45,7 @@ private theorem cons_lex_cons [BEq α] {lt : α → α → Bool} {a b : α} {xs
     cases a == b <;> simp
   · simp
 
-@[simp, grind =] theorem _root_.List.lex_toArray [BEq α] {lt : α → α → Bool} {l₁ l₂ : List α} :
+@[simp] theorem _root_.List.lex_toArray [BEq α] {lt : α → α → Bool} {l₁ l₂ : List α} :
     l₁.toArray.lex l₂.toArray lt = l₁.lex l₂ lt := by
   induction l₁ generalizing l₂ with
   | nil => cases l₂ <;> simp [lex, Id.run]
@@ -57,7 +55,7 @@ private theorem cons_lex_cons [BEq α] {lt : α → α → Bool} {a b : α} {xs
     | cons y l₂ =>
       rw [List.toArray_cons, List.toArray_cons y, cons_lex_cons, List.lex, ih]
 
-@[simp, grind =] theorem lex_toList [BEq α] {lt : α → α → Bool} {xs ys : Array α} :
+@[simp] theorem lex_toList [BEq α] {lt : α → α → Bool} {xs ys : Array α} :
     xs.toList.lex ys.toList lt = xs.lex ys lt := by
   cases xs <;> cases ys <;> simp
 

src/Init/Data/Array/MapIdx.lean

@@ -3,8 +3,6 @@ Copyright (c) 2022 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Kim Morrison
 -/
-module
-
 prelude
 import Init.Data.Array.Lemmas
 import Init.Data.Array.Attach
@@ -66,7 +64,7 @@ theorem mapFinIdx_spec {xs : Array α} {f : (i : Nat) → α → (h : i < xs.siz
 
 @[simp] theorem getElem?_mapFinIdx {xs : Array α} {f : (i : Nat) → α → (h : i < xs.size) → β} {i : Nat} :
     (xs.mapFinIdx f)[i]? =
-      xs[i]?.pbind fun b h => some <| f i b (getElem?_eq_some_iff.1 h).1 := by
+      xs[i]?.pbind fun b h => f i b (getElem?_eq_some_iff.1 h).1 := by
   simp only [getElem?_def, size_mapFinIdx, getElem_mapFinIdx]
   split <;> simp_all
 
@@ -111,11 +109,11 @@ end Array
 
 namespace List
 
-@[simp, grind =] theorem mapFinIdx_toArray {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} :
+@[simp] theorem mapFinIdx_toArray {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} :
     l.toArray.mapFinIdx f = (l.mapFinIdx f).toArray := by
   ext <;> simp
 
-@[simp, grind =] theorem mapIdx_toArray {f : Nat → α → β} {l : List α} :
+@[simp] theorem mapIdx_toArray {f : Nat → α → β} {l : List α} :
     l.toArray.mapIdx f = (l.mapIdx f).toArray := by
   ext <;> simp
 
@@ -132,7 +130,7 @@ namespace Array
 @[deprecated getElem_zipIdx (since := "2025-01-21")]
 abbrev getElem_zipWithIndex := @getElem_zipIdx
 
-@[simp, grind =] theorem zipIdx_toArray {l : List α} {k : Nat} :
+@[simp] theorem zipIdx_toArray {l : List α} {k : Nat} :
     l.toArray.zipIdx k = (l.zipIdx k).toArray := by
   ext i hi₁ hi₂ <;> simp [Nat.add_comm]
 
@@ -155,7 +153,7 @@ theorem mk_mem_zipIdx_iff_le_and_getElem?_sub {k i : Nat} {x : α} {xs : Array
 /-- Variant of `mk_mem_zipIdx_iff_le_and_getElem?_sub` specialized at `k = 0`,
 to avoid the inequality and the subtraction. -/
 theorem mk_mem_zipIdx_iff_getElem? {x : α} {i : Nat} {xs : Array α} :
-    (x, i) ∈ xs.zipIdx ↔ xs[i]? = some x := by
+    (x, i) ∈ xs.zipIdx ↔ xs[i]? = x := by
   rw [mk_mem_zipIdx_iff_le_and_getElem?_sub]
   simp
 
@@ -454,7 +452,7 @@ end Array
 
 namespace List
 
-@[grind] theorem mapFinIdxM_toArray [Monad m] [LawfulMonad m] {l : List α}
+theorem mapFinIdxM_toArray [Monad m] [LawfulMonad m] {l : List α}
     {f : (i : Nat) → α → (h : i < l.length) → m β} :
     l.toArray.mapFinIdxM f = toArray <$> l.mapFinIdxM f := by
   let rec go (i : Nat) (acc : Array β) (inv : i + acc.size = l.length) :
@@ -475,7 +473,7 @@ namespace List
   simp only [Array.mapFinIdxM, mapFinIdxM]
   exact go _ #[] _
 
-@[grind] theorem mapIdxM_toArray [Monad m] [LawfulMonad m] {l : List α}
+theorem mapIdxM_toArray [Monad m] [LawfulMonad m] {l : List α}
     {f : Nat → α → m β} :
     l.toArray.mapIdxM f = toArray <$> l.mapIdxM f := by
   let rec go (bs : List α) (acc : Array β) (inv : bs.length + acc.size = l.length) :

src/Init/Data/Array/Mem.lean

@@ -3,8 +3,6 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Joachim Breitner
 -/
-module
-
 prelude
 import Init.Data.Array.Basic
 import Init.Data.Nat.Linear

src/Init/Data/Array/Monadic.lean

@@ -3,8 +3,6 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
-module
-
 prelude
 import Init.Data.Array.Lemmas
 import Init.Data.Array.Attach
@@ -264,7 +262,7 @@ end Array
 
 namespace List
 
-@[grind =] theorem filterM_toArray [Monad m] [LawfulMonad m] {l : List α} {p : α → m Bool} :
+theorem filterM_toArray [Monad m] [LawfulMonad m] {l : List α} {p : α → m Bool} :
     l.toArray.filterM p = toArray <$> l.filterM p := by
   simp only [Array.filterM, filterM, foldlM_toArray, bind_pure_comp, Functor.map_map]
   conv => lhs; rw [← reverse_nil]
@@ -284,7 +282,7 @@ namespace List
   subst w
   rw [filterM_toArray]
 
-@[grind =] theorem filterRevM_toArray [Monad m] [LawfulMonad m] {l : List α} {p : α → m Bool} :
+theorem filterRevM_toArray [Monad m] [LawfulMonad m] {l : List α} {p : α → m Bool} :
     l.toArray.filterRevM p = toArray <$> l.filterRevM p := by
   simp [Array.filterRevM, filterRevM]
   rw [← foldlM_reverse, ← foldlM_toArray, ← Array.filterM, filterM_toArray]
@@ -296,7 +294,7 @@ namespace List
   subst w
   rw [filterRevM_toArray]
 
-@[grind =] theorem filterMapM_toArray [Monad m] [LawfulMonad m] {l : List α} {f : α → m (Option β)} :
+theorem filterMapM_toArray [Monad m] [LawfulMonad m] {l : List α} {f : α → m (Option β)} :
     l.toArray.filterMapM f = toArray <$> l.filterMapM f := by
   simp [Array.filterMapM, filterMapM]
   conv => lhs; rw [← reverse_nil]
@@ -314,7 +312,7 @@ namespace List
   subst w
   rw [filterMapM_toArray]
 
-@[simp, grind =] theorem flatMapM_toArray [Monad m] [LawfulMonad m] {l : List α} {f : α → m (Array β)} :
+@[simp] theorem flatMapM_toArray [Monad m] [LawfulMonad m] {l : List α} {f : α → m (Array β)} :
     l.toArray.flatMapM f = toArray <$> l.flatMapM (fun a => Array.toList <$> f a) := by
   simp only [Array.flatMapM, bind_pure_comp, foldlM_toArray, flatMapM]
   conv => lhs; arg 2; change [].reverse.flatten.toArray

src/Init/Data/Array/OfFn.lean

@@ -3,8 +3,6 @@ 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
 import Init.Data.Array.Lemmas
 import Init.Data.List.OfFn

src/Init/Data/Array/Perm.lean

@@ -3,8 +3,6 @@ Copyright (c) 2024 Lean FRO. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
-module
-
 prelude
 import Init.Data.List.Nat.Perm
 import Init.Data.Array.Lemmas
@@ -22,91 +20,56 @@ open List
 This is a wrapper around `List.Perm`, and for now has much less API.
 For more complicated verification, use `perm_iff_toList_perm` and the `List` API.
 -/
-structure Perm (as bs : Array α) : Prop where
-  of_toList_perm ::
-  toList : as.toList ~ bs.toList
+def Perm (as bs : Array α) : Prop :=
+  as.toList ~ bs.toList
 
 @[inherit_doc] scoped infixl:50 " ~ " => Perm
 
-theorem perm_iff_toList_perm {as bs : Array α} : as ~ bs ↔ as.toList ~ bs.toList :=
-  ⟨Perm.toList, Perm.of_toList_perm⟩
+theorem perm_iff_toList_perm {as bs : Array α} : as ~ bs ↔ as.toList ~ bs.toList := Iff.rfl
 
-end Array
-
-namespace List
-
-open Array
-
-theorem perm_iff_toArray_perm {as bs : List α} : as ~ bs ↔ as.toArray ~ bs.toArray := by
+@[simp] theorem perm_toArray (as bs : List α) : as.toArray ~ bs.toArray ↔ as ~ bs := by
   simp [perm_iff_toList_perm]
 
-theorem Perm.of_toArray_perm {as bs : List α} : as.toArray ~ bs.toArray → as ~ bs :=
-  perm_iff_toArray_perm.mpr
-
-theorem Perm.toArray {as bs : List α} : as ~ bs → as.toArray ~ bs.toArray :=
-  perm_iff_toArray_perm.mp
-
-end List
-
-namespace Array
-
-open List
-
 @[simp, refl] protected theorem Perm.refl (xs : Array α) : xs ~ xs := by
   cases xs
-  simp [perm_iff_toList_perm]
+  simp
 
 protected theorem Perm.rfl {xs : Array α} : xs ~ xs := .refl _
 
 theorem Perm.of_eq {xs ys : Array α} (h : xs = ys) : xs ~ ys := h ▸ .rfl
 
-@[symm]
 protected theorem Perm.symm {xs ys : Array α} (h : xs ~ ys) : ys ~ xs := by
   cases xs; cases ys
-  simp only [perm_iff_toList_perm] at h
-  simpa [perm_iff_toList_perm] using h.symm
+  simp only [perm_toArray] at h
+  simpa using h.symm
 
 protected theorem Perm.trans {xs ys zs : Array α} (h₁ : xs ~ ys) (h₂ : ys ~ zs) : xs ~ zs := by
   cases xs; cases ys; cases zs
-  simp only [perm_iff_toList_perm] at h₁ h₂
-  simpa [perm_iff_toList_perm] using h₁.trans h₂
+  simp only [perm_toArray] at h₁ h₂
+  simpa using h₁.trans h₂
 
 instance : Trans (Perm (α := α)) (Perm (α := α)) (Perm (α := α)) where
   trans h₁ h₂ := Perm.trans h₁ h₂
 
 theorem perm_comm {xs ys : Array α} : xs ~ ys ↔ ys ~ xs := ⟨Perm.symm, Perm.symm⟩
 
-theorem Perm.size_eq {xs ys : Array α} (p : xs ~ ys) : xs.size = ys.size := by
+theorem Perm.length_eq {xs ys : Array α} (p : xs ~ ys) : xs.size = ys.size := by
   cases xs; cases ys
-  simp only [perm_iff_toList_perm] at p
+  simp only [perm_toArray] at p
   simpa using p.length_eq
 
-@[deprecated Perm.size_eq (since := "2025-04-17")]
-abbrev Perm.length_eq := @Perm.size_eq
-
 theorem Perm.mem_iff {a : α} {xs ys : Array α} (p : xs ~ ys) : a ∈ xs ↔ a ∈ ys := by
   rcases xs with ⟨xs⟩
   rcases ys with ⟨ys⟩
-  simp only [perm_iff_toList_perm] at p
+  simp at p
   simpa using p.mem_iff
 
-theorem Perm.append {xs ys as bs : Array α} (p₁ : xs ~ ys) (p₂ : as ~ bs) :
-    xs ++ as ~ ys ++ bs := by
-  cases xs; cases ys; cases as; cases bs
-  simp only [append_toArray, perm_iff_toList_perm] at p₁ p₂ ⊢
-  exact p₁.append p₂
-
-theorem Perm.push (x : α) {xs ys : Array α} (p : xs ~ ys) :
-    xs.push x ~ ys.push x := by
-  rw [push_eq_append_singleton]
-  exact p.append .rfl
-
-theorem Perm.push_comm (x y : α) {xs ys : Array α} (p : xs ~ ys) :
+theorem Perm.push (x y : α) {xs ys : Array α} (p : xs ~ ys) :
     (xs.push x).push y ~ (ys.push y).push x := by
   cases xs; cases ys
-  simp only [perm_iff_toList_perm] at p
-  simp only [push_toArray, List.append_assoc, singleton_append, perm_iff_toList_perm]
-  exact p.append (Perm.swap ..)
+  simp only [perm_toArray] at p
+  simp only [push_toArray, List.append_assoc, singleton_append, perm_toArray]
+  exact p.append (Perm.swap' _ _ Perm.nil)
 
 theorem swap_perm {xs : Array α} {i j : Nat} (h₁ : i < xs.size) (h₂ : j < xs.size) :
     xs.swap i j ~ xs := by
@@ -118,10 +81,10 @@ namespace Perm
 set_option linter.indexVariables false in
 theorem extract {xs ys : Array α} (h : xs ~ ys) {lo hi : Nat}
     (wlo : ∀ i, i < lo → xs[i]? = ys[i]?) (whi : ∀ i, hi ≤ i → xs[i]? = ys[i]?) :
-    xs.extract lo hi ~ ys.extract lo hi := by
+    (xs.extract lo hi) ~ (ys.extract lo hi) := by
   rcases xs with ⟨xs⟩
   rcases ys with ⟨ys⟩
-  simp_all only [perm_iff_toList_perm, List.getElem?_toArray, List.extract_toArray,
+  simp_all only [perm_toArray, List.getElem?_toArray, List.extract_toArray,
     List.extract_eq_drop_take]
   apply List.Perm.take_of_getElem? (w := fun i h => by simpa using whi (lo + i) (by omega))
   apply List.Perm.drop_of_getElem? (w := wlo)

src/Init/Data/Array/QSort.lean

@@ -1,9 +1,68 @@
 /-
-Copyright (c) 2024 Lean FRO. All rights reserved.
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kim Morrison
+Authors: Leonardo de Moura
 -/
-module
-
 prelude
-import Init.Data.Array.QSort.Basic
+import Init.Data.Vector.Basic
+import Init.Data.Ord
+
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+-- We do not enable `linter.indexVariables` because it is helpful to name index variables `lo`, `mid`, `hi`, etc.
+
+namespace Array
+
+private def qpartition {n} (as : Vector α n) (lt : α → α → Bool) (lo hi : Nat)
+    (hlo : lo < n := by omega) (hhi : hi < n := by omega) : {n : Nat // lo ≤ n} × Vector α n :=
+  let mid := (lo + hi) / 2
+  let as  := if lt as[mid] as[lo] then as.swap lo mid else as
+  let as  := if lt as[hi]  as[lo] then as.swap lo hi  else as
+  let as  := if lt as[mid] as[hi] then as.swap mid hi else as
+  let pivot := as[hi]
+  let rec loop (as : Vector α n) (i j : Nat)
+      (ilo : lo ≤ i := by omega) (jh : j < n := by omega) (w : i ≤ j := by omega) :=
+    if h : j < hi then
+      if lt as[j] pivot then
+        loop (as.swap i j) (i+1) (j+1)
+      else
+        loop as i (j+1)
+    else
+      (⟨i, ilo⟩, as.swap i hi)
+  loop as lo lo
+
+/--
+Sorts an array using the Quicksort algorithm.
+
+The optional parameter `lt` specifies an ordering predicate. It defaults to `LT.lt`, which must be
+decidable to be used for sorting. Use `Array.qsortOrd` to sort the array according to the `Ord α`
+instance.
+
+The optional parameters `low` and `high` delimit the region of the array that is sorted. Both are
+inclusive, and default to sorting the entire array.
+-/
+@[inline] def qsort (as : Array α) (lt : α → α → Bool := by exact (· < ·))
+    (low := 0) (high := as.size - 1) : Array α :=
+  let rec @[specialize] sort {n} (as : Vector α n) (lo hi : Nat)
+      (hlo : lo < n := by omega) (hhi : hi < n := by omega) :=
+    if h₁ : lo < hi then
+      let ⟨⟨mid, hmid⟩, as⟩ := qpartition as lt lo hi
+      if h₂ : mid ≥ hi then
+        as
+      else
+        sort (sort as lo mid) (mid+1) hi
+    else as
+  if h : as.size = 0 then
+    as
+  else
+    let low := min low (as.size - 1)
+    let high := min high (as.size - 1)
+    sort ⟨as, rfl⟩ low high |>.toArray
+
+set_option linter.unusedVariables.funArgs false in
+/--
+Sorts an array using the Quicksort algorithm, using `Ord.compare` to compare elements.
+-/
+def qsortOrd [ord : Ord α] (xs : Array α) : Array α :=
+  xs.qsort fun x y => compare x y |>.isLT
+
+end Array

src/Init/Data/Array/QSort/Basic.lean

@@ -1,81 +0,0 @@
-/-
-Copyright (c) 2019 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-module
-
-prelude
-import Init.Data.Vector.Basic
-import Init.Data.Ord
-
-set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- We do not enable `linter.indexVariables` because it is helpful to name index variables `lo`, `mid`, `hi`, etc.
-
-
-namespace Array
-
-/--
-Internal implementation of `Array.qsort`.
-
-`qpartition as lt lo hi hlo hhi` returns a pair `(⟨m, h₁, h₂⟩, as')` where
-`as'` is a permutation of `as` and `m` is a number such that:
-- `lo ≤ m`
-- `m < n`
-- `∀ i, lo ≤ i → i < m → lt as[i] as[m]`
-- `∀ j, m < j → j < hi → !lt as[j] as[m]`
-
-It does so by first swapping the elements at indices `lo`, `mid := (lo + hi) / 2`, and `hi`
-if necessary so that the middle (pivot) element is at index `hi`.
-We then iterate from `j = lo` to `j = hi`, with a pointer `i` starting at `lo`, and
-swapping each element which is less than the pivot to position `i`, and then incrementing `i`.
--/
-def qpartition {n} (as : Vector α n) (lt : α → α → Bool) (lo hi : Nat)
-    (hlo : lo < n := by omega) (hhi : hi < n := by omega) : {m : Nat // lo ≤ m ∧ m < n} × Vector α n :=
-  let mid := (lo + hi) / 2
-  let as  := if lt as[mid] as[lo] then as.swap lo mid else as
-  let as  := if lt as[hi]  as[lo] then as.swap lo hi  else as
-  let as  := if lt as[mid] as[hi] then as.swap mid hi else as
-  let pivot := as[hi]
-  let rec loop (as : Vector α n) (i j : Nat)
-      (ilo : lo ≤ i := by omega) (jh : j < n := by omega) (w : i ≤ j := by omega) :=
-    if h : j < hi then
-      if lt as[j] pivot then
-        loop (as.swap i j) (i+1) (j+1)
-      else
-        loop as i (j+1)
-    else
-      (⟨i, ilo, by omega⟩, as.swap i hi)
-  loop as lo lo
-
-/--
-In-place quicksort.
-
-`qsort as lt low high` sorts the subarray `as[low:high+1]` in-place using `lt` to compare elements.
--/
-@[inline] def qsort (as : Array α) (lt : α → α → Bool := by exact (· < ·))
-    (low := 0) (high := as.size - 1) : Array α :=
-  let rec @[specialize] sort {n} (as : Vector α n) (lo hi : Nat)
-      (hlo : lo < n := by omega) (hhi : hi < n := by omega) :=
-    if h₁ : lo < hi then
-      let ⟨⟨mid, hmid⟩, as⟩ := qpartition as lt lo hi
-      if h₂ : mid ≥ hi then
-        as
-      else
-        sort (sort as lo mid) (mid+1) hi
-    else as
-  if h : as.size = 0 then
-    as
-  else
-    let low := min low (as.size - 1)
-    let high := min high (as.size - 1)
-    sort as.toVector low high |>.toArray
-
-set_option linter.unusedVariables.funArgs false in
-/--
-Sort an array using `compare` to compare elements.
--/
-def qsortOrd [ord : Ord α] (xs : Array α) : Array α :=
-  xs.qsort fun x y => compare x y |>.isLT
-
-end Array

src/Init/Data/Array/Range.lean

@@ -3,8 +3,6 @@ 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
 import Init.Data.Array.Lemmas
 import Init.Data.Array.OfFn

src/Init/Data/Array/Set.lean

@@ -3,8 +3,6 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Mario Carneiro
 -/
-module
-
 prelude
 import Init.Tactics
 

src/Init/Data/Array/Subarray.lean

@@ -3,8 +3,6 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-module
-
 prelude
 import Init.Data.Array.Basic
 
@@ -464,12 +462,8 @@ instance : Append (Subarray α) where
    let a := x.toArray ++ y.toArray
    a.toSubarray 0 a.size
 
-/-- `Subarray` representation. -/
-protected def Subarray.repr [Repr α] (s : Subarray α) : Std.Format :=
-  repr s.toArray ++ ".toSubarray"
-
 instance [Repr α] : Repr (Subarray α) where
-  reprPrec s  _ := Subarray.repr s
+  reprPrec s  _ := repr s.toArray ++ ".toSubarray"
 
 instance [ToString α] : ToString (Subarray α) where
   toString s := toString s.toArray

src/Init/Data/Array/Subarray/Split.lean

@@ -4,8 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: David Thrane Christiansen
 -/
 
-module
-
 prelude
 import Init.Data.Array.Basic
 import Init.Data.Array.Subarray

src/Init/Data/Array/TakeDrop.lean

@@ -3,8 +3,6 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel
 -/
-module
-
 prelude
 import Init.Data.Array.Lemmas
 import Init.Data.List.Nat.TakeDrop

src/Init/Data/Array/Zip.lean

@@ -3,8 +3,6 @@ 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
 import Init.Data.Array.TakeDrop
 import Init.Data.List.Zip
@@ -325,7 +323,7 @@ theorem map_zipWithAll {δ : Type _} {f : α → β} {g : Option γ → Option
   simp [List.map_zipWithAll]
 
 @[simp] theorem zipWithAll_replicate {a : α} {b : β} {n : Nat} :
-    zipWithAll f (replicate n a) (replicate n b) = replicate n (f (some a) (some b)) := by
+    zipWithAll f (replicate n a) (replicate n b) = replicate n (f a b) := by
   simp [← List.toArray_replicate]
 
 @[deprecated zipWithAll_replicate (since := "2025-03-18")]

src/Init/Data/BEq.lean

@@ -3,8 +3,6 @@ Copyright (c) 2022 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Markus Himmel
 -/
-module
-
 prelude
 import Init.Data.Bool
 
@@ -27,7 +25,7 @@ class EquivBEq (α) [BEq α] : Prop extends PartialEquivBEq α, ReflBEq α
 theorem BEq.symm [BEq α] [PartialEquivBEq α] {a b : α} : a == b → b == a :=
   PartialEquivBEq.symm
 
-@[grind] theorem BEq.comm [BEq α] [PartialEquivBEq α] {a b : α} : (a == b) = (b == a) :=
+theorem BEq.comm [BEq α] [PartialEquivBEq α] {a b : α} : (a == b) = (b == a) :=
   Bool.eq_iff_iff.2 ⟨BEq.symm, BEq.symm⟩
 
 theorem bne_comm [BEq α] [PartialEquivBEq α] {a b : α} : (a != b) = (b != a) := by

src/Init/Data/Basic.lean

@@ -3,8 +3,6 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-module
-
 prelude
 import Init.Data.Nat.Basic
 import Init.Data.Fin.Basic

src/Init/Data/BitVec.lean

@@ -3,8 +3,6 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
-module
-
 prelude
 import Init.Data.BitVec.Basic
 import Init.Data.BitVec.Bitblast

src/Init/Data/BitVec/Basic.lean

@@ -3,8 +3,6 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joe Hendrix, Wojciech Nawrocki, Leonardo de Moura, Mario Carneiro, Alex Keizer, Harun Khan, Abdalrhman M Mohamed, Siddharth Bhat
 -/
-module
-
 prelude
 import Init.Data.Fin.Basic
 import Init.Data.Nat.Bitwise.Lemmas
@@ -150,7 +148,7 @@ with `BitVec.toInt` results in the value `i.bmod (2^n)`.
 protected def ofInt (n : Nat) (i : Int) : BitVec n := .ofNatLT (i % (Int.ofNat (2^n))).toNat (by
   apply (Int.toNat_lt _).mpr
   · apply Int.emod_lt_of_pos
-    exact Int.natCast_pos.mpr (Nat.two_pow_pos _)
+    exact Int.ofNat_pos.mpr (Nat.two_pow_pos _)
   · apply Int.emod_nonneg
     intro eq
     apply Nat.ne_of_gt (Nat.two_pow_pos n)
@@ -199,13 +197,7 @@ protected def toHex {n : Nat} (x : BitVec n) : String :=
   let t := (List.replicate ((n+3) / 4 - s.length) '0').asString
   t ++ s
 
-/-- `BitVec` representation. -/
-protected def BitVec.repr (a : BitVec n) : Std.Format :=
-  "0x" ++ (a.toHex : Std.Format) ++ "#" ++ repr n
-
-instance : Repr (BitVec n) where
-  reprPrec a _ := BitVec.repr a
-
+instance : Repr (BitVec n) where reprPrec a _ := "0x" ++ (a.toHex : Std.Format) ++ "#" ++ repr n
 instance : ToString (BitVec n) where toString a := toString (repr a)
 
 end repr_toString
@@ -436,6 +428,8 @@ def setWidth' {n w : Nat} (le : n ≤ w) (x : BitVec n) : BitVec w :=
     apply Nat.lt_of_lt_of_le x.isLt
     exact Nat.pow_le_pow_right (by trivial) le)
 
+@[deprecated setWidth' (since := "2024-09-18"), inherit_doc setWidth'] abbrev zeroExtend' := @setWidth'
+
 /--
 Returns `zeroExtend (w+n) x <<< n` without needing to compute `x % 2^(2+n)`.
 -/
@@ -773,15 +767,6 @@ SMT-Lib name: `bvnego`.
 def negOverflow {w : Nat} (x : BitVec w) : Bool :=
   x.toInt == - 2 ^ (w - 1)
 
-/--
-Checks whether the signed division of `x` by `y` results in overflow.
-For BitVecs `x` and `y` with nonzero width, this only happens if `x = intMin` and `y = allOnes w`.
-
-SMT-LIB name: `bvsdivo`.
--/
-def sdivOverflow {w : Nat} (x y : BitVec w) : Bool :=
-  (2 ^ (w - 1) ≤ x.toInt / y.toInt) || (x.toInt / y.toInt <  - 2 ^ (w - 1))
-
 /- ### reverse -/
 
 /-- Reverses the bits in a bitvector. -/

src/Init/Data/BitVec/BasicAux.lean

@@ -3,8 +3,6 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joe Hendrix, Wojciech Nawrocki, Leonardo de Moura, Mario Carneiro, Alex Keizer, Harun Khan, Abdalrhman M Mohamed
 -/
-module
-
 prelude
 import Init.Data.Fin.Basic
 

src/Init/Data/BitVec/Bitblast.lean

@@ -3,8 +3,6 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Harun Khan, Abdalrhman M Mohamed, Joe Hendrix, Siddharth Bhat
 -/
-module
-
 prelude
 import Init.Data.BitVec.Folds
 import Init.Data.Nat.Mod
@@ -516,7 +514,7 @@ theorem msb_neg {w : Nat} {x : BitVec w} :
   rw [(show w = w - 1 + 1 by omega), Int.pow_succ] at this
   omega
 
-@[simp] theorem setWidth_neg_of_le {x : BitVec v} (h : w ≤ v) : BitVec.setWidth w (-x) = -BitVec.setWidth w x := by
+@[simp] theorem BitVec.setWidth_neg_of_le {x : BitVec v} (h : w ≤ v) : BitVec.setWidth w (-x) = -BitVec.setWidth w x := by
   simp [← BitVec.signExtend_eq_setWidth_of_le _ h, BitVec.signExtend_neg_of_le h]
 
 /-! ### abs -/
@@ -668,6 +666,11 @@ theorem setWidth_setWidth_succ_eq_setWidth_setWidth_add_twoPow (x : BitVec w) (i
       getLsbD_zero, and_eq_false_imp, and_eq_true, decide_eq_true_eq, and_imp]
     by_cases hi : x.getLsbD i <;> simp [hi] <;> omega
 
+@[deprecated setWidth_setWidth_succ_eq_setWidth_setWidth_add_twoPow (since := "2024-09-18"),
+  inherit_doc setWidth_setWidth_succ_eq_setWidth_setWidth_add_twoPow]
+abbrev zeroExtend_truncate_succ_eq_zeroExtend_truncate_add_twoPow :=
+  @setWidth_setWidth_succ_eq_setWidth_setWidth_add_twoPow
+
 /--
 Recurrence lemma: multiplying `x` with the first `s` bits of `y` is the
 same as truncating `y` to `s` bits, then zero extending to the original length,
@@ -694,6 +697,10 @@ theorem mulRec_eq_mul_signExtend_setWidth (x y : BitVec w) (s : Nat) :
       by_cases hy : y.getLsbD (s' + 1) <;> simp [hy]
     rw [heq, ← BitVec.mul_add, ← setWidth_setWidth_succ_eq_setWidth_setWidth_add_twoPow]
 
+@[deprecated mulRec_eq_mul_signExtend_setWidth (since := "2024-09-18"),
+  inherit_doc mulRec_eq_mul_signExtend_setWidth]
+abbrev mulRec_eq_mul_signExtend_truncate := @mulRec_eq_mul_signExtend_setWidth
+
 theorem getLsbD_mul (x y : BitVec w) (i : Nat) :
     (x * y).getLsbD i = (mulRec x y w).getLsbD i := by
   simp only [mulRec_eq_mul_signExtend_setWidth]
@@ -1349,41 +1356,9 @@ theorem negOverflow_eq {w : Nat} (x : BitVec w) :
   rcases w with _|w
   · simp [toInt_of_zero_length, Int.min_eq_right]
   · suffices - 2 ^ w = (intMin (w + 1)).toInt by simp [beq_eq_decide_eq, ← toInt_inj, this]
-    simp only [toInt_intMin, Nat.add_one_sub_one, Int.natCast_emod, Int.neg_inj]
+    simp only [toInt_intMin, Nat.add_one_sub_one, Int.ofNat_emod, Int.neg_inj]
     rw_mod_cast [Nat.mod_eq_of_lt (by simp [Nat.pow_lt_pow_succ])]
 
-/--
-  Prove that signed division `x.toInt / y.toInt` only overflows when `x = intMin w` and `y = allOnes w` (for `0 < w`).
--/
-theorem sdivOverflow_eq {w : Nat} (x y : BitVec w) :
-    (sdivOverflow x y) = (decide (0 < w) && (x = intMin w) && (y = allOnes w)) := by
-  rcases w with _|w
-  · simp [sdivOverflow, of_length_zero]
-  · have yle := le_two_mul_toInt (x := y)
-    have ylt := two_mul_toInt_lt (x := y)
-    -- if y = allOnes (w + 1), thus y.toInt = -1,
-    -- the division overflows iff x = intMin (w + 1), as for negation
-    by_cases hy : y = allOnes (w + 1)
-    · simp [sdivOverflow_eq_negOverflow_of_eq_allOnes, negOverflow_eq, ← hy, beq_eq_decide_eq]
-    · simp only [sdivOverflow, hy, bool_to_prop]
-      have := BitVec.neg_two_pow_le_toInt_ediv (x := x) (y := y)
-      simp only [Nat.add_one_sub_one] at this
-      by_cases hx : 0 ≤ x.toInt
-      · by_cases hy' : 0 ≤ y.toInt
-        · have := BitVec.toInt_ediv_toInt_lt_of_nonneg_of_nonneg
-                (x := x) (y := y) (by omega) (by omega)
-          simp only [Nat.add_one_sub_one] at this; simp; omega
-        · have := BitVec.toInt_ediv_toInt_nonpos_of_nonneg_of_nonpos
-                (x := x) (y := y) (by omega) (by omega)
-          simp; omega
-      · by_cases hy' : 0 ≤ y.toInt
-        · have :=  BitVec.toInt_ediv_toInt_nonpos_of_nonpos_of_nonneg
-                (x := x) (y := y) (by omega) (by omega)
-          simp; omega
-        · have := BitVec.toInt_ediv_toInt_lt_of_nonpos_of_lt_neg_one
-                (x := x) (y := y) (by omega) (by rw [← toInt_inj, toInt_allOnes] at hy; omega)
-          simp only [Nat.add_one_sub_one] at this; simp; omega
-
 theorem umulOverflow_eq {w : Nat} (x y : BitVec w) :
     umulOverflow x y =
       (0 < w && BitVec.twoPow (w * 2) w ≤ x.zeroExtend (w * 2) * y.zeroExtend (w * 2)) := by
@@ -1492,6 +1467,7 @@ theorem sdiv_intMin {x : BitVec w} :
   by_cases h : x = intMin w
   · subst h
     simp
+    omega
   · simp only [sdiv_eq, msb_intMin, show 0 < w by omega, h]
     have := Nat.two_pow_pos (w-1)
     by_cases hx : x.msb
@@ -1564,7 +1540,7 @@ theorem sdiv_ne_intMin_of_ne_intMin {x y : BitVec w} (h : x ≠ intMin w) :
 
 theorem toInt_eq_neg_toNat_neg_of_msb_true {x : BitVec w} (h : x.msb = true) :
     x.toInt = -((-x).toNat) := by
-  simp only [toInt_eq_msb_cond, h, ↓reduceIte, toNat_neg, Int.natCast_emod]
+  simp only [toInt_eq_msb_cond, h, ↓reduceIte, toNat_neg, Int.ofNat_emod]
   norm_cast
   rw [Nat.mod_eq_of_lt]
   · omega
@@ -1659,7 +1635,7 @@ theorem toInt_sdiv_of_ne_or_ne (a b : BitVec w) (h : a ≠ intMin w ∨ b ≠ -1
           (a.sdiv b).toInt = -((-a).toNat / b.toNat) := by
         simp only [sdiv_eq, ha, hb, udiv_eq]
         rw [toInt_eq_neg_toNat_neg_of_nonpos]
-        · rw [neg_neg, toNat_udiv, toNat_neg, Int.natCast_emod, Int.neg_inj]
+        · rw [neg_neg, toNat_udiv, toNat_neg, Int.ofNat_emod, Int.neg_inj]
           norm_cast
         · rw [neg_eq_zero_iff]
           by_cases h' : -a / b = 0#w
@@ -1802,23 +1778,9 @@ theorem extractLsb'_mul {w len} {x y : BitVec w} (hlen : len ≤ w) :
     (x * y).extractLsb' 0 len = (x.extractLsb' 0 len) * (y.extractLsb' 0 len) := by
   simp [← setWidth_eq_extractLsb' hlen, setWidth_mul _ _ hlen]
 
-/-- Adding bitvectors that are zero in complementary positions equals concatenation.
-We add a `no_index` annotation to `HAppend.hAppend` such that the width `v + w`
-does not act as a key in the discrimination tree.
-This is important to allow matching, when the type of the result of append
-`x : BitVec 3` and `y : BitVec 4` has been reduced to `x ++ y : BitVec 7`.
--/
-theorem append_zero_add_zero_append {v w : Nat} {x : BitVec v} {y : BitVec w} :
-    (HAppend.hAppend (γ := BitVec (no_index _)) x 0#w) +
-    (HAppend.hAppend (γ := BitVec (no_index _)) 0#v y)
-    = x ++ y := by
-  rw [add_eq_or_of_and_eq_zero] <;> ext i <;> simp
-
 /-- Adding bitvectors that are zero in complementary positions equals concatenation. -/
-theorem zero_append_add_append_zero {v w : Nat} {x : BitVec v} {y : BitVec w} :
-  (HAppend.hAppend (γ := BitVec (no_index _)) 0#v y) +
-  (HAppend.hAppend (γ := BitVec (no_index _)) x 0#w)
-  = x ++ y := by
+theorem append_add_append_eq_append {v w : Nat} {x : BitVec v} {y : BitVec w} :
+    (x ++ 0#w) + (0#v ++ y) = x ++ y := by
   rw [add_eq_or_of_and_eq_zero] <;> ext i <;> simp
 
 /-- Heuristically, `y <<< x` is much larger than `x`,
@@ -1834,10 +1796,4 @@ theorem add_shiftLeft_eq_or_shiftLeft {x y : BitVec w} :
   have : i < 2^i := by exact Nat.lt_two_pow_self
   omega
 
-/-- Heuristically, `y <<< x` is much larger than `x`,
-and hence low bits of `y <<< x`. Thus, `(y <<< x) + x = (y <<< x) ||| x.` -/
-theorem shiftLeft_add_eq_shiftLeft_or {x y : BitVec w} :
-    (y <<< x) + x =  (y <<< x) ||| x := by
-  rw [BitVec.add_comm, add_shiftLeft_eq_or_shiftLeft, or_comm]
-
 end BitVec

src/Init/Data/BitVec/Folds.lean

@@ -3,8 +3,6 @@ Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joe Hendrix, Harun Khan
 -/
-module
-
 prelude
 import Init.Data.BitVec.Lemmas
 import Init.Data.Nat.Lemmas

src/Init/Data/BitVec/Lemmas.lean

@@ -4,8 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joe Hendrix, Harun Khan, Alex Keizer, Abdalrhman M Mohamed, Siddharth Bhat
 
 -/
-module
-
 prelude
 import Init.Data.Bool
 import Init.Data.BitVec.Basic
@@ -23,9 +21,6 @@ set_option linter.missingDocs true
 
 namespace BitVec
 
-@[simp] theorem mk_zero : BitVec.ofFin (w := w) ⟨0, h⟩ = 0#w := rfl
-@[simp] theorem ofNatLT_zero : BitVec.ofNatLT (w := w) 0 h = 0#w := rfl
-
 @[simp] theorem getLsbD_ofFin (x : Fin (2^n)) (i : Nat) :
     getLsbD (BitVec.ofFin x) i = x.val.testBit i := rfl
 
@@ -141,8 +136,6 @@ theorem toNat_ne_iff_ne {n} {x y : BitVec n} : x.toNat ≠ y.toNat ↔ x ≠ y :
 @[bitvec_to_nat] theorem toNat_eq {x y : BitVec n} : x = y ↔ x.toNat = y.toNat :=
   Iff.intro (congrArg BitVec.toNat) eq_of_toNat_eq
 
-theorem toNat_inj {x y : BitVec n} : x.toNat = y.toNat ↔ x = y := toNat_eq.symm
-
 @[bitvec_to_nat] theorem toNat_ne {x y : BitVec n} : x ≠ y ↔ x.toNat ≠ y.toNat := by
   rw [Ne, toNat_eq]
 
@@ -315,12 +308,6 @@ theorem ofFin_ofNat (n : Nat) :
     ofFin (no_index (OfNat.ofNat n : Fin (2^w))) = OfNat.ofNat n := by
   simp only [OfNat.ofNat, Fin.ofNat', BitVec.ofNat, Nat.and_two_pow_sub_one_eq_mod]
 
-@[simp] theorem ofFin_neg {x : Fin (2 ^ w)} : ofFin (-x) = -(ofFin x) := by
-  rfl
-
-@[simp, norm_cast] theorem ofFin_natCast (n : Nat) : ofFin (n : Fin (2^w)) = (n : BitVec w) := by
-  rfl
-
 theorem eq_of_toFin_eq : ∀ {x y : BitVec w}, x.toFin = y.toFin → x = y
   | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
 
@@ -336,9 +323,6 @@ theorem toFin_zero : toFin (0 : BitVec w) = 0 := rfl
 theorem toFin_one  : toFin (1 : BitVec w) = 1 := by
   rw [toFin_inj]; simp only [ofNat_eq_ofNat, ofFin_ofNat]
 
-@[simp, norm_cast] theorem toFin_natCast (n : Nat) : toFin (n : BitVec w) = (n : Fin (2^w)) := by
-  rfl
-
 @[simp] theorem toNat_ofBool (b : Bool) : (ofBool b).toNat = b.toNat := by
   cases b <;> rfl
 
@@ -527,10 +511,6 @@ theorem getElem_ofBool {b : Bool} {h : i < 1}: (ofBool b)[i] = b := by
   · rintro rfl
     simp
 
-/-- `0#w = 1#w` iff the width is zero. -/
-@[simp] theorem zero_eq_one_iff (w : Nat) : (0#w = 1#w) ↔ (w = 0) := by
-  rw [← one_eq_zero_iff, eq_comm]
-
 /-! ### msb -/
 
 @[simp] theorem msb_zero : (0#w).msb = false := by simp [BitVec.msb, getMsbD]
@@ -633,10 +613,10 @@ theorem toInt_eq_toNat_bmod (x : BitVec n) : x.toInt = Int.bmod x.toNat (2^n) :=
   simp only [toInt_eq_toNat_cond]
   split
   next g =>
-    rw [Int.bmod_pos] <;> simp only [←Int.natCast_emod, toNat_mod_cancel]
+    rw [Int.bmod_pos] <;> simp only [←Int.ofNat_emod, toNat_mod_cancel]
     omega
   next g =>
-    rw [Int.bmod_neg] <;> simp only [←Int.natCast_emod, toNat_mod_cancel]
+    rw [Int.bmod_neg] <;> simp only [←Int.ofNat_emod, toNat_mod_cancel]
     omega
 
 theorem toInt_neg_of_msb_true {x : BitVec w} (h : x.msb = true) : x.toInt < 0 := by
@@ -652,12 +632,12 @@ theorem toInt_nonneg_of_msb_false {x : BitVec w} (h : x.msb = false) : 0 ≤ x.t
 @[simp] theorem toInt_one_of_lt {w : Nat} (h : 1 < w) : (1#w).toInt = 1 := by
   rw [toInt_eq_msb_cond]
   simp only [msb_one, show w ≠ 1 by omega, decide_false, Bool.false_eq_true, ↓reduceIte,
-    toNat_ofNat, Int.natCast_emod]
+    toNat_ofNat, Int.ofNat_emod]
   norm_cast
   apply Nat.mod_eq_of_lt
   apply Nat.one_lt_two_pow (by omega)
 
-/-- Prove equality of bitvectors in terms of integer operations. -/
+/-- Prove equality of bitvectors in terms of nat operations. -/
 theorem eq_of_toInt_eq {x y : BitVec n} : x.toInt = y.toInt → x = y := by
   intro eq
   simp only [toInt_eq_toNat_cond] at eq
@@ -681,10 +661,6 @@ theorem toInt_ne {x y : BitVec n} : x.toInt ≠ y.toInt ↔ x ≠ y  := by
 theorem toInt_ofNat {n : Nat} (x : Nat) : (BitVec.ofNat n x).toInt = (x : Int).bmod (2^n) := by
   simp [toInt_eq_toNat_bmod, -Int.natCast_pow]
 
-@[simp] theorem toInt_ofFin {w : Nat} (x : Fin (2^w)) :
-    (BitVec.ofFin x).toInt = Int.bmod x (2^w) := by
-  simp [toInt_eq_toNat_bmod]
-
 @[simp] theorem toInt_ofInt {n : Nat} (i : Int) :
   (BitVec.ofInt n i).toInt = i.bmod (2^n) := by
   have _ := Nat.two_pow_pos n
@@ -790,6 +766,7 @@ theorem le_two_mul_toInt {w : Nat} {x : BitVec w} : -2 ^ w ≤ 2 * x.toInt := by
     simp only [Nat.zero_lt_succ, Nat.mul_lt_mul_left, Int.natCast_mul, Int.cast_ofNat_Int]
     norm_cast; omega
 
+
 theorem le_toInt {w : Nat} (x : BitVec w) : -2 ^ (w - 1) ≤ x.toInt := by
   by_cases h : w = 0
   · subst h
@@ -805,17 +782,6 @@ theorem le_toInt {w : Nat} (x : BitVec w) : -2 ^ (w - 1) ≤ x.toInt := by
   · simpa [Int.mul_comm _ 2] using le_two_mul_toInt
   · simpa [Int.mul_comm _ 2] using two_mul_toInt_lt
 
-@[simp] theorem toNat_intCast {w : Nat} (x : Int) : (x : BitVec w).toNat = (x % 2^w).toNat := by
-  change (BitVec.ofInt w x).toNat = _
-  simp
-
-@[simp] theorem toInt_intCast {w : Nat} (x : Int) : (x : BitVec w).toInt = Int.bmod x (2^w) := by
-  rw [toInt_eq_toNat_bmod, toNat_intCast, Int.natCast_toNat_eq_self.mpr]
-  · have h : (2 ^ w : Int) = (2 ^ w : Nat) := by simp
-    rw [h, Int.emod_bmod]
-  · apply Int.emod_nonneg
-    exact Int.pow_ne_zero (by decide)
-
 /-! ### sle/slt -/
 
 /--
@@ -2575,7 +2541,7 @@ where
       simp [getElem_signExtend, Nat.le_sub_one_of_lt hv]
       omega
     have H : 2^w ≤ 2^v := Nat.pow_le_pow_right (by omega) (by omega)
-    simp only [this, toNat_setWidth, Int.natCast_add, Int.natCast_emod, Int.natCast_mul]
+    simp only [this, toNat_setWidth, Int.natCast_add, Int.ofNat_emod, Int.natCast_mul]
     by_cases h : x.msb
     <;> norm_cast
     <;> simp [h, Nat.mod_eq_of_lt (Nat.lt_of_lt_of_le x.isLt H), -Int.natCast_pow]
@@ -3109,6 +3075,10 @@ theorem setWidth_succ (x : BitVec w) :
     · simp_all
     · omega
 
+@[deprecated "Use the reverse direction of `cons_msb_setWidth`" (since := "2024-09-23")]
+theorem eq_msb_cons_setWidth (x : BitVec (w+1)) : x = (cons x.msb (x.setWidth w)) := by
+  simp
+
 @[simp] theorem not_cons (x : BitVec w) (b : Bool) : ~~~(cons b x) = cons (!b) (~~~x) := by
   simp [cons]
 
@@ -3894,7 +3864,7 @@ theorem le_zero_iff {x : BitVec w} : x ≤ 0#w ↔ x = 0#w := by
 theorem lt_one_iff {x : BitVec w} (h : 0 < w) : x < 1#w ↔ x = 0#w := by
   constructor
   · intro h₂
-    rw [lt_def, toNat_ofNat, ← Int.ofNat_lt, Int.natCast_emod, Int.ofNat_one, Int.natCast_pow,
+    rw [lt_def, toNat_ofNat, ← Int.ofNat_lt, Int.ofNat_emod, Int.ofNat_one, Int.natCast_pow,
       Int.ofNat_two, @Int.emod_eq_of_lt 1 (2^w) (by omega) (by omega)] at h₂
     simp [toNat_eq, show x.toNat = 0 by omega]
   · simp_all
@@ -4173,110 +4143,6 @@ theorem sdiv_self {x : BitVec w} :
       rcases x.msb with msb | msb <;> simp
     · rcases x.msb with msb | msb <;> simp [h]
 
-/-- Unsigned division never overflows. -/
-theorem toNat_div_toNat_lt {w : Nat} {x y : BitVec w} :
-    x.toNat / y.toNat < 2 ^ w := by
-  have hy : y.toNat = 0 ∨ y.toNat = 1 ∨ 1 < y.toNat := by omega
-  rcases hy with hy|hy|hy
-  · simp [hy]; omega
-  · simp [hy]; omega
-  · rw [Nat.div_lt_iff_lt_mul (k := y.toNat) (x := x.toNat) (y := 2 ^ w) (by omega), show x.toNat = x.toNat * 1 by omega]
-    apply Nat.mul_lt_mul_of_le_of_lt (by omega) (by omega) (by omega)
-
-/-- Non-overflowing signed division bounds when numerator is nonneg, denominator is nonneg. -/
-theorem toInt_ediv_toInt_lt_of_nonneg_of_nonneg {w : Nat} {x y : BitVec w} (hx : 0 ≤ x.toInt) (hy : 0 ≤ y.toInt) :
-    x.toInt / y.toInt < 2 ^ (w - 1) := by
-  rcases w with _|w
-  · simp [of_length_zero]
-  · have xle := le_two_mul_toInt (x := x); have xlt := two_mul_toInt_lt (x := x)
-    by_cases hy' : y.toInt = 1
-    · simp [hy', Int.ediv_one]; omega
-    · by_cases hx' : x.toInt = 0
-      · simp only [hx', Int.zero_ediv, Nat.add_one_sub_one, gt_iff_lt]
-        norm_cast
-        exact Nat.two_pow_pos (w := w)
-      · have := Int.ediv_lt_self_of_pos_of_ne_one (x := x.toInt) (y := y.toInt) (by omega) (by omega)
-        simp; omega
-
-/-- Non-overflowing signed division bounds when numerator is nonpos, denominator is nonneg. -/
-theorem toInt_ediv_toInt_nonpos_of_nonpos_of_nonneg {w : Nat} {x y : BitVec w} (hx : x.toInt ≤ 0) (hy : 0 ≤ y.toInt) :
-    x.toInt / y.toInt ≤ 0 := by
-  rcases w with _|w
-  · simp [of_length_zero]
-  · by_cases hx' : x.toInt = 0
-    · simp [hx']
-    · by_cases hy' : y.toInt = 0
-      · simp [hy']
-      · have := Int.ediv_neg_of_neg_of_pos (a := x.toInt) (b := y.toInt) (by omega) (by omega)
-        simp; omega
-
-/-- Non-overflowing signed division bounds when numerator is nonneg, denominator is nonpos. -/
-theorem toInt_ediv_toInt_nonpos_of_nonneg_of_nonpos {w : Nat} {x y : BitVec w} (hx : 0 ≤ x.toInt) (hy : y.toInt ≤ 0) :
-   x.toInt / y.toInt ≤ 0 := by
-  rcases w with _|w
-  · simp [of_length_zero]
-  · by_cases hy' : y.toInt = -1
-    · simp [hy']; omega
-    · have := Int.ediv_nonpos_of_nonneg_of_nonpos (a := x.toInt) (b := y.toInt) (by omega) (by omega)
-      simp; omega
-
-/-- Given the definition of ediv/emod for signed integer division (https://dl.acm.org/doi/pdf/10.1145/128861.128862)
-  we have that for two integers `x` and `y`: `x/y = q ↔ x.ediv y = q ↔ r = x.emod y`
-  and in particular: `-1/y = q ↔ -1.ediv y = q ↔ r = -1.emod y`.
-  from which it follows that:
-  (-1)/0 = 0
-  (-1)/y = -1 when 0 < y
-  (-1)/(-5) = 1 when y < 0
--/
-theorem neg_one_ediv_toInt_eq {w : Nat} {y : BitVec w} :
-    (-1) / y.toInt = if y.toInt = 0 then 0 else if 0 < y.toInt then -1 else 1 := by
-  rcases w with _|_|w
-  · simp [of_length_zero]
-  · cases eq_zero_or_eq_one y
-    · case _ h => simp [h]
-    · case _ h => simp [h]
-  · by_cases 0 < y.toInt
-    · simp [Int.sign_eq_one_of_pos (a := y.toInt) (by omega), Int.neg_one_ediv]
-      omega
-    · by_cases hy : y.toInt = 0
-      · simp [hy]
-      · simp [Int.sign_eq_neg_one_of_neg (a := y.toInt) (by omega), Int.neg_one_ediv]
-        omega
-
-/-- Non-overflowing signed division bounds when numerator is nonpos, denominator is less than -1. -/
-theorem toInt_ediv_toInt_lt_of_nonpos_of_lt_neg_one {w : Nat} {x y : BitVec w} (hx : x.toInt ≤ 0) (hy : y.toInt < -1) :
-    x.toInt / y.toInt < 2 ^ (w - 1) := by
-  rcases w with _|_|w
-  · simp [of_length_zero]
-  · have hy := eq_zero_or_eq_one (a := y)
-    simp [← toInt_inj, toInt_zero, toInt_one] at hy
-    omega
-  · have xle := le_two_mul_toInt (x := x); have xlt := two_mul_toInt_lt (x := x)
-    have hx' : x.toInt = 0 ∨ x.toInt = - 1 ∨ x.toInt < - 1 := by omega
-    rcases hx' with hx'|hx'|hx'
-    · simp [hx']; omega
-    · have := BitVec.neg_one_ediv_toInt_eq (y := y)
-      simp only [toInt_allOnes, Nat.lt_add_left_iff_pos, Nat.zero_lt_succ, ↓reduceIte,
-        Int.reduceNeg] at this
-      simp [hx', this]
-      omega
-    · have := Int.ediv_lt_natAbs_self_of_lt_neg_one_of_lt_neg_one (x := x.toInt) (y := y.toInt) (by omega) hy
-      simp; omega
-
-/-- Signed division of (x y : BitVec w) is always -2 ^ w ≤ x.toInt / y.toInt. -/
-theorem neg_two_pow_le_toInt_ediv {x y : BitVec w} :
-    - 2 ^ (w - 1) ≤ x.toInt / y.toInt := by
-  have xlt := @toInt_lt w x; have lex := @le_toInt w x
-  by_cases hx : 0 ≤ x.toInt <;> by_cases hy : 0 ≤ y.toInt
-  · have := Int.ediv_nonneg_of_nonneg_of_nonneg (x := x.toInt) (y := y.toInt) hx hy
-    omega
-  · have := Int.neg_self_le_ediv_of_nonneg_of_nonpos (x := x.toInt) (y := y.toInt) hx (by omega)
-    omega
-  · have := Int.self_le_ediv_of_nonpos_of_nonneg (x := x.toInt) (y := y.toInt) (by omega) hy
-    omega
-  · have := Int.ediv_nonneg_of_nonpos_of_nonpos (a := x.toInt) (b := y.toInt) (by omega) (by omega)
-    omega
-
 /-! ### smtSDiv -/
 
 theorem smtSDiv_eq (x y : BitVec w) : smtSDiv x y =
@@ -5079,7 +4945,7 @@ theorem toInt_intMin_le (x : BitVec w) :
   cases w
   case zero => simp [toInt_intMin, @of_length_zero x]
   case succ w =>
-    simp only [toInt_intMin, Nat.add_one_sub_one, Int.natCast_emod]
+    simp only [toInt_intMin, Nat.add_one_sub_one, Int.ofNat_emod]
     have : 0 < 2 ^ w := Nat.two_pow_pos w
     rw [Int.emod_eq_of_lt (by omega) (by omega)]
     rw [BitVec.toInt_eq_toNat_bmod]
@@ -5274,22 +5140,6 @@ theorem sub_le_sub_iff_le {x y z : BitVec w} (hxz : z ≤ x) (hyz : z ≤ y) :
     BitVec.toNat_sub_of_le (by rw [BitVec.le_def]; omega)]
   omega
 
-theorem sdiv_neg_one {w : Nat} {x : BitVec w} :
-    x.toInt / -1 = -x.toInt := by
-  rcases w with _|w
-  · simp [of_length_zero]
-  · simp [toInt_allOnes]
-
-theorem sdivOverflow_eq_negOverflow_of_eq_allOnes {w : Nat} {x y : BitVec w} (hy : y = allOnes w) :
-    sdivOverflow x y = negOverflow x := by
-  rcases w with _|w
-  · simp [sdivOverflow, negOverflow, of_length_zero]
-  · have xle := le_two_mul_toInt (x := x); have xlt := two_mul_toInt_lt (x := x)
-    simp only [sdivOverflow, hy, show ¬2 ^ w < x.toInt by omega, negOverflow]
-    by_cases hx : x.toInt = - 2 ^ w
-    · simp [hx]
-    · simp [show ¬x.toInt == -2 ^ w by simp only [beq_iff_eq, hx, not_false_eq_true]]; omega
-
 theorem two_pow_le_toInt_mul_toInt_iff {x y : BitVec w} :
     2 ^ (w - 1) ≤ x.toInt * y.toInt ↔
       (signExtend (w * 2) (intMax w)).slt (signExtend (w * 2) x * signExtend (w * 2) y) := by
@@ -5335,14 +5185,6 @@ theorem msb_eq_toNat {x : BitVec w}:
     x.msb = decide (x.toNat ≥ 2 ^ (w - 1)) := by
   simp only [msb_eq_decide, ge_iff_le]
 
-/-- Negating a bitvector created from a natural number equals
-creating a bitvector from the the negative of that number.
--/
-theorem neg_ofNat_eq_ofInt_neg {w : Nat} {x : Nat} :
-    - BitVec.ofNat w x = BitVec.ofInt w (- x) := by
-  apply BitVec.eq_of_toInt_eq
-  simp [BitVec.toInt_neg, BitVec.toInt_ofNat]
-
 /-! ### abs -/
 
 theorem abs_eq (x : BitVec w) : x.abs = if x.msb then -x else x := by rfl
@@ -5578,6 +5420,150 @@ abbrev toFin_uShiftRight := @toFin_ushiftRight
 @[deprecated signExtend_eq_setWidth_of_msb_false (since := "2024-12-08")]
 abbrev signExtend_eq_not_setWidth_not_of_msb_false := @signExtend_eq_setWidth_of_msb_false
 
+@[deprecated truncate_eq_setWidth (since := "2024-09-18")]
+abbrev truncate_eq_zeroExtend := @truncate_eq_setWidth
+
+@[deprecated toNat_setWidth' (since := "2024-09-18")]
+abbrev toNat_zeroExtend' := @toNat_setWidth'
+
+@[deprecated toNat_setWidth (since := "2024-09-18")]
+abbrev toNat_zeroExtend := @toNat_setWidth
+
+@[deprecated toNat_setWidth (since := "2024-09-18")]
+abbrev toNat_truncate := @toNat_setWidth
+
+@[deprecated setWidth_eq (since := "2024-09-18")]
+abbrev zeroExtend_eq := @setWidth_eq
+
+@[deprecated setWidth_eq (since := "2024-09-18")]
+abbrev truncate_eq := @setWidth_eq
+
+@[deprecated setWidth_zero (since := "2024-09-18")]
+abbrev zeroExtend_zero := @setWidth_zero
+
+@[deprecated getElem_setWidth (since := "2024-09-18")]
+abbrev getElem_zeroExtend := @getElem_setWidth
+
+@[deprecated getElem_setWidth' (since := "2024-09-18")]
+abbrev getElem_zeroExtend' := @getElem_setWidth'
+
+@[deprecated getElem?_setWidth (since := "2024-09-18")]
+abbrev getElem?_zeroExtend := @getElem?_setWidth
+
+@[deprecated getElem?_setWidth' (since := "2024-09-18")]
+abbrev getElem?_zeroExtend' := @getElem?_setWidth'
+
+@[deprecated getLsbD_setWidth (since := "2024-09-18")]
+abbrev getLsbD_zeroExtend := @getLsbD_setWidth
+
+@[deprecated getLsbD_setWidth' (since := "2024-09-18")]
+abbrev getLsbD_zeroExtend' := @getLsbD_setWidth'
+
+@[deprecated getMsbD_setWidth_add (since := "2024-09-18")]
+abbrev getMsbD_zeroExtend_add := @getMsbD_setWidth_add
+
+@[deprecated getMsbD_setWidth' (since := "2024-09-18")]
+abbrev getMsbD_zeroExtend' := @getMsbD_setWidth'
+
+@[deprecated getElem_setWidth (since := "2024-09-18")]
+abbrev getElem_truncate := @getElem_setWidth
+
+@[deprecated getElem?_setWidth (since := "2024-09-18")]
+abbrev getElem?_truncate := @getElem?_setWidth
+
+@[deprecated getLsbD_setWidth (since := "2024-09-18")]
+abbrev getLsbD_truncate := @getLsbD_setWidth
+
+@[deprecated msb_setWidth (since := "2024-09-18")]
+abbrev msb_truncate := @msb_setWidth
+
+@[deprecated cast_setWidth (since := "2024-09-18")]
+abbrev cast_zeroExtend := @cast_setWidth
+
+@[deprecated cast_setWidth (since := "2024-09-18")]
+abbrev cast_truncate := @cast_setWidth
+
+@[deprecated setWidth_setWidth_of_le (since := "2024-09-18")]
+abbrev zeroExtend_zeroExtend_of_le := @setWidth_setWidth_of_le
+
+@[deprecated setWidth_eq (since := "2024-09-18")]
+abbrev truncate_eq_self := @setWidth_eq
+
+@[deprecated setWidth_cast (since := "2024-09-18")]
+abbrev truncate_cast := @setWidth_cast
+
+@[deprecated msb_setWidth (since := "2024-09-18")]
+abbrev mbs_zeroExtend := @msb_setWidth
+
+@[deprecated msb_setWidth' (since := "2024-09-18")]
+abbrev mbs_zeroExtend' := @msb_setWidth'
+
+@[deprecated setWidth_one_eq_ofBool_getLsb_zero (since := "2024-09-18")]
+abbrev zeroExtend_one_eq_ofBool_getLsb_zero := @setWidth_one_eq_ofBool_getLsb_zero
+
+@[deprecated setWidth_ofNat_one_eq_ofNat_one_of_lt (since := "2024-09-18")]
+abbrev zeroExtend_ofNat_one_eq_ofNat_one_of_lt := @setWidth_ofNat_one_eq_ofNat_one_of_lt
+
+@[deprecated setWidth_one (since := "2024-09-18")]
+abbrev truncate_one := @setWidth_one
+
+@[deprecated setWidth_ofNat_of_le (since := "2024-09-18")]
+abbrev truncate_ofNat_of_le := @setWidth_ofNat_of_le
+
+@[deprecated setWidth_or (since := "2024-09-18")]
+abbrev truncate_or := @setWidth_or
+
+@[deprecated setWidth_and (since := "2024-09-18")]
+abbrev truncate_and := @setWidth_and
+
+@[deprecated setWidth_xor (since := "2024-09-18")]
+abbrev truncate_xor := @setWidth_xor
+
+@[deprecated setWidth_not (since := "2024-09-18")]
+abbrev truncate_not := @setWidth_not
+
+@[deprecated signExtend_eq_setWidth_of_msb_false  (since := "2024-09-18")]
+abbrev signExtend_eq_not_zeroExtend_not_of_msb_false  := @signExtend_eq_setWidth_of_msb_false
+
+@[deprecated signExtend_eq_not_setWidth_not_of_msb_true (since := "2024-09-18")]
+abbrev signExtend_eq_not_zeroExtend_not_of_msb_true := @signExtend_eq_not_setWidth_not_of_msb_true
+
+@[deprecated signExtend_eq_setWidth_of_lt (since := "2024-09-18")]
+abbrev signExtend_eq_truncate_of_lt := @signExtend_eq_setWidth_of_le
+
+@[deprecated truncate_append (since := "2024-09-18")]
+abbrev truncate_append := @setWidth_append
+
+@[deprecated truncate_append_of_eq (since := "2024-09-18")]
+abbrev truncate_append_of_eq := @setWidth_append_of_eq
+
+@[deprecated truncate_cons (since := "2024-09-18")]
+abbrev truncate_cons := @setWidth_cons
+
+@[deprecated truncate_succ (since := "2024-09-18")]
+abbrev truncate_succ := @setWidth_succ
+
+@[deprecated truncate_add (since := "2024-09-18")]
+abbrev truncate_add := @setWidth_add
+
+@[deprecated setWidth_setWidth_succ_eq_setWidth_setWidth_of_getLsbD_false (since := "2024-09-18")]
+abbrev zeroExtend_truncate_succ_eq_zeroExtend_truncate_of_getLsbD_false := @setWidth_setWidth_succ_eq_setWidth_setWidth_of_getLsbD_false
+
+@[deprecated setWidth_setWidth_succ_eq_setWidth_setWidth_or_twoPow_of_getLsbD_true (since := "2024-09-18")]
+abbrev zeroExtend_truncate_succ_eq_zeroExtend_truncate_or_twoPow_of_getLsbD_true := @setWidth_setWidth_succ_eq_setWidth_setWidth_or_twoPow_of_getLsbD_true
+
+@[deprecated and_one_eq_setWidth_ofBool_getLsbD (since := "2024-09-18")]
+abbrev and_one_eq_zeroExtend_ofBool_getLsbD := @and_one_eq_setWidth_ofBool_getLsbD
+
+@[deprecated msb_sshiftRight (since := "2024-10-03")]
+abbrev sshiftRight_msb_eq_msb := @msb_sshiftRight
+
+@[deprecated shiftLeft_zero (since := "2024-10-27")]
+abbrev shiftLeft_zero_eq := @shiftLeft_zero
+
+@[deprecated ushiftRight_zero (since := "2024-10-27")]
+abbrev ushiftRight_zero_eq := @ushiftRight_zero
+
 @[deprecated replicate_zero (since := "2025-01-08")]
 abbrev replicate_zero_eq := @replicate_zero
 

src/Init/Data/Bool.lean

@@ -3,8 +3,6 @@ Copyright (c) 2023 F. G. Dorais. No rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: F. G. Dorais
 -/
-module
-
 prelude
 import Init.NotationExtra
 

src/Init/Data/ByteArray.lean

@@ -3,7 +3,5 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
-module
-
 prelude
 import Init.Data.ByteArray.Basic

src/Init/Data/ByteArray/Basic.lean

@@ -3,8 +3,6 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
-module
-
 prelude
 import Init.Data.Array.Basic
 import Init.Data.Array.Subarray

src/Init/Data/Cast.lean

@@ -3,8 +3,6 @@ Copyright (c) 2014 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Gabriel Ebner
 -/
-module
-
 prelude
 import Init.Coe
 

src/Init/Data/Char.lean

@@ -3,8 +3,6 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-module
-
 prelude
 import Init.Data.Char.Basic
 import Init.Data.Char.Lemmas

src/Init/Data/Char/Basic.lean

@@ -3,8 +3,6 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
-module
-
 prelude
 import Init.Data.UInt.BasicAux
 

src/Init/Data/Char/Lemmas.lean

@@ -3,8 +3,6 @@ Copyright (c) 2024 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
 import Init.Data.Char.Basic
 import Init.Data.UInt.Lemmas

src/Init/Data/Fin.lean

@@ -3,8 +3,6 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
-module
-
 prelude
 import Init.Data.Fin.Basic
 import Init.Data.Fin.Log2

src/Init/Data/Fin/Basic.lean

@@ -3,8 +3,6 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura, Robert Y. Lewis, Keeley Hoek, Mario Carneiro
 -/
-module
-
 prelude
 import Init.Data.Nat.Bitwise.Basic
 
@@ -230,19 +228,6 @@ instance : ShiftRight (Fin n) where
 instance instOfNat {n : Nat} [NeZero n] {i : Nat} : OfNat (Fin n) i where
   ofNat := Fin.ofNat' n i
 
-/-- If you actually have an element of `Fin n`, then the `n` is always positive -/
-protected theorem pos (i : Fin n) : 0 < n :=
-  Nat.lt_of_le_of_lt (Nat.zero_le _) i.2
-
-/-- Negation on `Fin n` -/
-instance neg (n : Nat) : Neg (Fin n) :=
-  ⟨fun a => ⟨(n - a) % n, Nat.mod_lt _ a.pos⟩⟩
-
-theorem neg_def (a : Fin n) : -a = ⟨(n - a) % n, Nat.mod_lt _ a.pos⟩ := rfl
-
-protected theorem coe_neg (a : Fin n) : ((-a : Fin n) : Nat) = (n - a) % n :=
-  rfl
-
 instance instInhabited {n : Nat} [NeZero n] : Inhabited (Fin n) where
   default := 0
 
@@ -260,6 +245,10 @@ theorem modn_lt : ∀ {m : Nat} (i : Fin n), m > 0 → (modn i m).val < m
 theorem val_lt_of_le (i : Fin b) (h : b ≤ n) : i.val < n :=
   Nat.lt_of_lt_of_le i.isLt h
 
+/-- If you actually have an element of `Fin n`, then the `n` is always positive -/
+protected theorem pos (i : Fin n) : 0 < n :=
+  Nat.lt_of_le_of_lt (Nat.zero_le _) i.2
+
 /--
 The greatest value of `Fin (n+1)`, namely `n`.
 

src/Init/Data/Fin/Bitwise.lean

@@ -3,8 +3,6 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel
 -/
-module
-
 prelude
 import Init.Data.Nat.Bitwise
 import Init.Data.Fin.Basic

src/Init/Data/Fin/Fold.lean

@@ -3,8 +3,6 @@ Copyright (c) 2023 François G. Dorais. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: François G. Dorais
 -/
-module
-
 prelude
 import Init.Data.Nat.Linear
 import Init.Control.Lawful.Basic

src/Init/Data/Fin/Iterate.lean

@@ -3,8 +3,6 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joe Hendrix
 -/
-module
-
 prelude
 import Init.PropLemmas
 import Init.Data.Fin.Basic

src/Init/Data/Fin/Lemmas.lean

@@ -3,12 +3,9 @@ Copyright (c) 2022 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Leonardo de Moura
 -/
-module
-
 prelude
 import Init.Data.Fin.Basic
 import Init.Data.Nat.Lemmas
-import Init.Data.Int.DivMod.Lemmas
 import Init.Ext
 import Init.ByCases
 import Init.Conv
@@ -100,21 +97,6 @@ theorem dite_val {n : Nat} {c : Prop} [Decidable c] {x y : Fin n} :
     (if c then x else y).val = if c then x.val else y.val := by
   by_cases c <;> simp [*]
 
-instance (n : Nat) [NeZero n] : NatCast (Fin n) where
-  natCast a := Fin.ofNat' n a
-
-def intCast [NeZero n] (a : Int) : Fin n :=
-  if 0 ≤ a then
-    Fin.ofNat' n a.natAbs
-  else
-    - Fin.ofNat' n a.natAbs
-
-instance (n : Nat) [NeZero n] : IntCast (Fin n) where
-  intCast := Fin.intCast
-
-theorem intCast_def {n : Nat} [NeZero n] (x : Int) :
-    (x : Fin n) = if 0 ≤ x then Fin.ofNat' n x.natAbs else -Fin.ofNat' n x.natAbs := rfl
-
 /-! ### order -/
 
 theorem le_def {a b : Fin n} : a ≤ b ↔ a.1 ≤ b.1 := .rfl
@@ -172,7 +154,7 @@ protected theorem eq_or_lt_of_le {a b : Fin n} : a ≤ b → a = b ∨ a < b :=
 protected theorem lt_or_eq_of_le {a b : Fin n} : a ≤ b → a < b ∨ a = b := by
   rw [Fin.ext_iff]; exact Nat.lt_or_eq_of_le
 
-theorem is_le (i : Fin (n + 1)) : i.1 ≤ n := Nat.le_of_lt_succ i.is_lt
+theorem is_le (i : Fin (n + 1)) : i ≤ n := Nat.le_of_lt_succ i.is_lt
 
 @[simp] theorem is_le' {a : Fin n} : a ≤ n := Nat.le_of_lt a.is_lt
 
@@ -190,13 +172,13 @@ theorem mk_le_of_le_val {b : Fin n} {a : Nat} (h : a ≤ b) :
 
 @[simp] theorem mk_zero : (⟨0, Nat.succ_pos n⟩ : Fin (n + 1)) = 0 := rfl
 
-@[simp] theorem zero_le [NeZero n] (a : Fin n) : 0 ≤ a := Nat.zero_le a.val
+@[simp] theorem zero_le (a : Fin (n + 1)) : 0 ≤ a := Nat.zero_le a.val
 
 theorem zero_lt_one : (0 : Fin (n + 2)) < 1 := Nat.zero_lt_one
 
-@[simp] theorem not_lt_zero [NeZero n] (a : Fin n) : ¬a < 0 := nofun
+@[simp] theorem not_lt_zero (a : Fin (n + 1)) : ¬a < 0 := nofun
 
-theorem pos_iff_ne_zero [NeZero n] {a : Fin n} : 0 < a ↔ a ≠ 0 := by
+theorem pos_iff_ne_zero {a : Fin (n + 1)} : 0 < a ↔ a ≠ 0 := by
   rw [lt_def, val_zero, Nat.pos_iff_ne_zero, ← val_ne_iff]; rfl
 
 theorem eq_zero_or_eq_succ {n : Nat} : ∀ i : Fin (n + 1), i = 0 ∨ ∃ j : Fin n, i = j.succ
@@ -235,7 +217,7 @@ theorem rev_eq {n a : Nat} (i : Fin (n + 1)) (h : n = a + i) :
 
 /-! ### last -/
 
-@[simp] theorem val_last (n : Nat) : (last n).1 = n := rfl
+@[simp] theorem val_last (n : Nat) : last n = n := rfl
 
 @[simp] theorem last_zero : (Fin.last 0 : Fin 1) = 0 := by
   ext
@@ -276,7 +258,7 @@ theorem subsingleton_iff_le_one : Subsingleton (Fin n) ↔ n ≤ 1 := by
   (match n with | 0 | 1 | n+2 => ?_) <;> try simp
   · exact ⟨nofun⟩
   · exact ⟨fun ⟨0, _⟩ ⟨0, _⟩ => rfl⟩
-  · exact fun h => by have := zero_lt_one (n := n); simp_all [h.elim 0 1]
+  · exact iff_of_false (fun h => Fin.ne_of_lt zero_lt_one (h.elim ..)) (of_decide_eq_false rfl)
 
 instance subsingleton_zero : Subsingleton (Fin 0) := subsingleton_iff_le_one.2 (by decide)
 
@@ -428,14 +410,6 @@ theorem succ_succ_ne_one (a : Fin n) : Fin.succ (Fin.succ a) ≠ 1 :=
 
 @[simp] theorem coe_cast (h : n = m) (i : Fin n) : (i.cast h : Nat) = i := rfl
 
-@[simp] theorem cast_castLE {k m n} (km : k ≤ m) (mn : m = n) (i : Fin k) :
-    Fin.cast mn (i.castLE km) = i.castLE (mn ▸ km) :=
-  Fin.ext (by simp)
-
-@[simp] theorem cast_castLT {k m n} (i : Fin k) (h : (i : Nat) < m) (mn : m = n) :
-    Fin.cast mn (i.castLT h) = i.castLT (mn ▸ h) :=
-  Fin.ext (by simp)
-
 @[simp] theorem cast_zero [NeZero n] [NeZero m] (h : n = m) : Fin.cast h 0 = 0 := rfl
 
 @[simp] theorem cast_last {n' : Nat} {h : n + 1 = n' + 1} : (last n).cast h  = last n' :=
@@ -522,17 +496,17 @@ theorem castSucc_inj {a b : Fin n} : a.castSucc = b.castSucc ↔ a = b := by sim
 
 theorem castSucc_lt_last (a : Fin n) : a.castSucc < last n := a.is_lt
 
-@[simp] theorem castSucc_zero [NeZero n] : castSucc (0 : Fin n) = 0 := rfl
+@[simp] theorem castSucc_zero : castSucc (0 : Fin (n + 1)) = 0 := rfl
 
 @[simp] theorem castSucc_one {n : Nat} : castSucc (1 : Fin (n + 2)) = 1 := rfl
 
 /-- `castSucc i` is positive when `i` is positive -/
-theorem castSucc_pos [NeZero n] {i : Fin n} (h : 0 < i) : 0 < i.castSucc := by
+theorem castSucc_pos {i : Fin (n + 1)} (h : 0 < i) : 0 < i.castSucc := by
   simpa [lt_def] using h
 
-@[simp] theorem castSucc_eq_zero_iff [NeZero n] {a : Fin n} : a.castSucc = 0 ↔ a = 0 := by simp [Fin.ext_iff]
+@[simp] theorem castSucc_eq_zero_iff {a : Fin (n + 1)} : a.castSucc = 0 ↔ a = 0 := by simp [Fin.ext_iff]
 
-theorem castSucc_ne_zero_iff [NeZero n] {a : Fin n} : a.castSucc ≠ 0 ↔ a ≠ 0 :=
+theorem castSucc_ne_zero_iff {a : Fin (n + 1)} : a.castSucc ≠ 0 ↔ a ≠ 0 :=
   not_congr <| castSucc_eq_zero_iff
 
 theorem castSucc_fin_succ (n : Nat) (j : Fin n) :
@@ -941,15 +915,6 @@ theorem addCases_right {m n : Nat} {motive : Fin (m + n) → Sort _} {left right
   have : ¬(natAdd m i : Nat) < m := Nat.not_lt.2 (le_coe_natAdd ..)
   rw [addCases, dif_neg this]; exact eq_of_heq <| (eqRec_heq _ _).trans (by congr 1; simp)
 
-/-! ### zero -/
-
-@[simp, norm_cast]
-theorem val_eq_zero_iff [NeZero n] {a : Fin n} : a.val = 0 ↔ a = 0 := by
-  rw [Fin.ext_iff, val_zero]
-
-theorem val_ne_zero_iff [NeZero n] {a : Fin n} : a.val ≠ 0 ↔ a ≠ 0 :=
-  not_congr val_eq_zero_iff
-
 /-! ### add -/
 
 theorem ofNat'_add [NeZero n] (x : Nat) (y : Fin n) :
@@ -1009,17 +974,6 @@ theorem coe_sub_iff_lt {a b : Fin n} : (↑(a - b) : Nat) = n + a - b ↔ a < b
     rw [Nat.mod_eq_of_lt]
     all_goals omega
 
-/-! ### neg -/
-
-theorem val_neg {n : Nat} [NeZero n] (x : Fin n) :
-    (-x).val = if x = 0 then 0 else n - x.val := by
-  change (n - ↑x) % n = _
-  split <;> rename_i h
-  · simp_all
-  · rw [Nat.mod_eq_of_lt]
-    have := Fin.val_ne_zero_iff.mpr h
-    omega
-
 /-! ### mul -/
 
 theorem ofNat'_mul [NeZero n] (x : Nat) (y : Fin n) :
@@ -1038,12 +992,10 @@ theorem val_mul {n : Nat} : ∀ a b : Fin n, (a * b).val = a.val * b.val % n
 theorem coe_mul {n : Nat} : ∀ a b : Fin n, ((a * b : Fin n) : Nat) = a * b % n
   | ⟨_, _⟩, ⟨_, _⟩ => rfl
 
-protected theorem mul_one [i : NeZero n] (k : Fin n) : k * 1 = k := by
-  match n, i with
-  | n + 1, _ =>
-    match n with
-    | 0 => exact Subsingleton.elim (α := Fin 1) ..
-    | n+1 => simp [Fin.ext_iff, mul_def, Nat.mod_eq_of_lt (is_lt k)]
+protected theorem mul_one (k : Fin (n + 1)) : k * 1 = k := by
+  match n with
+  | 0 => exact Subsingleton.elim (α := Fin 1) ..
+  | n+1 => simp [Fin.ext_iff, mul_def, Nat.mod_eq_of_lt (is_lt k)]
 
 protected theorem mul_comm (a b : Fin n) : a * b = b * a :=
   Fin.ext <| by rw [mul_def, mul_def, Nat.mul_comm]
@@ -1056,17 +1008,15 @@ protected theorem mul_assoc (a b c : Fin n) : a * b * c = a * (b * c) := by
   simp only [← Nat.mul_mod, Nat.mul_assoc]
 instance : Std.Associative (α := Fin n) (· * ·) := ⟨Fin.mul_assoc⟩
 
-protected theorem one_mul [NeZero n] (k : Fin n) : (1 : Fin n) * k = k := by
+protected theorem one_mul (k : Fin (n + 1)) : (1 : Fin (n + 1)) * k = k := by
   rw [Fin.mul_comm, Fin.mul_one]
-
-instance [NeZero n] : Std.LawfulIdentity (α := Fin n) (· * ·) 1 where
+instance : Std.LawfulIdentity (α := Fin (n + 1)) (· * ·) 1 where
   left_id := Fin.one_mul
   right_id := Fin.mul_one
 
-protected theorem mul_zero [NeZero n] (k : Fin n) : k * 0 = 0 := by
-  simp [Fin.ext_iff, mul_def]
+protected theorem mul_zero (k : Fin (n + 1)) : k * 0 = 0 := by simp [Fin.ext_iff, mul_def]
 
-protected theorem zero_mul [NeZero n] (k : Fin n) : (0 : Fin n) * k = 0 := by
+protected theorem zero_mul (k : Fin (n + 1)) : (0 : Fin (n + 1)) * k = 0 := by
   simp [Fin.ext_iff, mul_def]
 
 end Fin

src/Init/Data/Fin/Log2.lean

@@ -3,8 +3,6 @@ Copyright (c) 2022 Henrik Böving. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
-module
-
 prelude
 import Init.Data.Nat.Log2
 

src/Init/Data/Float.lean

@@ -3,8 +3,6 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-module
-
 prelude
 import Init.Core
 import Init.Data.Int.Basic
@@ -291,11 +289,8 @@ implementation.
 instance : Inhabited Float where
   default := UInt64.toFloat 0
 
-protected def Float.repr (n : Float) (prec : Nat) : Std.Format :=
-  if n < UInt64.toFloat 0 then Repr.addAppParen (toString n) prec else toString n
-
 instance : Repr Float where
-  reprPrec := Float.repr
+  reprPrec n prec := if n < UInt64.toFloat 0 then Repr.addAppParen (toString n) prec else toString n
 
 instance : ReprAtom Float  := ⟨⟩
 

src/Init/Data/Float32.lean

@@ -3,8 +3,6 @@ Copyright (c) 2023 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
 import Init.Core
 import Init.Data.Int.Basic
@@ -292,11 +290,8 @@ implementation.
 instance : Inhabited Float32 where
   default := UInt64.toFloat32 0
 
-protected def Float32.repr (n : Float32) (prec : Nat) : Std.Format :=
-  if n < UInt64.toFloat32 0 then Repr.addAppParen (toString n) prec else toString n
-
 instance : Repr Float32 where
-  reprPrec := Float32.repr
+  reprPrec n prec := if n < UInt64.toFloat32 0 then Repr.addAppParen (toString n) prec else toString n
 
 instance : ReprAtom Float32  := ⟨⟩
 

src/Init/Data/FloatArray.lean

@@ -3,7 +3,5 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
-module
-
 prelude
 import Init.Data.FloatArray.Basic