Update src/Lean/Meta/Tactic/Apply.lean

Co-authored-by: Kyle Miller <kmill31415@gmail.com>

.github/workflows/ci.yml

@@ -62,7 +62,7 @@ jobs:
                 "os": "ubuntu-latest",
                 "release": false,
                 "quick": false,
-                "shell": "nix develop .#oldGlibc -c bash -euxo pipefail {0}",
+                "shell": "nix-shell --arg pkgsDist \"import (fetchTarball \\\"channel:nixos-19.03\\\") {{}}\" --run \"bash -euxo pipefail {0}\"",
                 "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",
@@ -76,7 +76,7 @@ jobs:
                 "os": "ubuntu-latest",
                 "release": true,
                 "quick": true,
-                "shell": "nix develop .#oldGlibc -c bash -euxo pipefail {0}",
+                "shell": "nix-shell --arg pkgsDist \"import (fetchTarball \\\"channel:nixos-19.03\\\") {{}}\" --run \"bash -euxo pipefail {0}\"",
                 "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",
@@ -98,8 +98,7 @@ jobs:
                 // exclude seriously slow tests
                 "CTEST_OPTIONS": "-E 'interactivetest|leanpkgtest|laketest|benchtest'"
               },
-              // TODO: suddenly started failing in CI
-              /*{
+              {
                 "name": "Linux fsanitize",
                 "os": "ubuntu-latest",
                 "quick": false,
@@ -107,7 +106,7 @@ jobs:
                 "CMAKE_OPTIONS": "-DLEAN_EXTRA_CXX_FLAGS=-fsanitize=address,undefined -DLEANC_EXTRA_FLAGS='-fsanitize=address,undefined -fsanitize-link-c++-runtime' -DSMALL_ALLOCATOR=OFF -DBSYMBOLIC=OFF",
                 // exclude seriously slow/problematic tests (laketests crash)
                 "CTEST_OPTIONS": "-E 'interactivetest|leanpkgtest|laketest|benchtest'"
-              },*/
+              },
               {
                 "name": "macOS",
                 "os": "macos-latest",
@@ -141,10 +140,12 @@ jobs:
                 "shell": "msys2 {0}",
                 "CMAKE_OPTIONS": "-G \"Unix Makefiles\" -DUSE_GMP=OFF",
                 // for reasons unknown, interactivetests are flaky on Windows
-                "CTEST_OPTIONS": "--repeat until-pass:2",
+                // also, the liasolver test hits “too many exported symbols”
+                "CTEST_OPTIONS": "--repeat until-pass:2 -E 'leanbenchtest_liasolver.lean'",
                 "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"
+                // TEMP while compiler tests are deactivated
+                "binary-check": "true"
               },
               {
                 "name": "Linux aarch64",
@@ -154,7 +155,7 @@ jobs:
                 "quick": false,
                 "cross": true,
                 "cross_target": "aarch64-unknown-linux-gnu",
-                "shell": "nix develop .#oldGlibcAArch -c bash -euxo pipefail {0}",
+                "shell": "nix-shell --arg pkgsDist \"import (fetchTarball \\\"channel:nixos-19.03\\\") {{ localSystem.config = \\\"aarch64-unknown-linux-gnu\\\"; }}\" --run \"bash -euxo pipefail {0}\"",
                 "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-linux-gnu.tar.zst 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-aarch64-* lean-llvm-x86_64-*"
               },
@@ -252,7 +253,7 @@ jobs:
     runs-on: ${{ matrix.os }}
     defaults:
       run:
-        shell: ${{ matrix.shell || 'nix develop -c bash -euxo pipefail {0}' }}
+        shell: ${{ matrix.shell || 'nix-shell --run "bash -euxo pipefail {0}"' }}
     name: ${{ matrix.name }}
     env:
       # must be inside workspace
@@ -383,14 +384,8 @@ jobs:
           cd build/stage1
           ulimit -c unlimited # coredumps
           # exclude nonreproducible test
-          ctest -j4 --progress --output-junit test-results.xml --output-on-failure ${{ matrix.CTEST_OPTIONS }} < /dev/null
+          ctest -j4 --output-on-failure ${{ matrix.CTEST_OPTIONS }} < /dev/null
         if: (matrix.wasm || !matrix.cross) && needs.configure.outputs.quick == 'false'
-      - name: Test Summary
-        uses: test-summary/action@v2
-        with:
-          paths: build/stage1/test-results.xml
-        # prefix `if` above with `always` so it's run even if tests failed
-        if: always() && (matrix.wasm || !matrix.cross) && needs.configure.outputs.quick == 'false'
       - name: Check Test Binary
         run: ${{ matrix.binary-check }} tests/compiler/534.lean.out
         if: ${{ !matrix.cross && needs.configure.outputs.quick == 'false' }}
@@ -452,10 +447,9 @@ jobs:
     name: Build matrix complete
     runs-on: ubuntu-latest
     needs: build
-    # mark as merely cancelled not failed if builds are cancelled
-    if: ${{ !cancelled() }}
+    if: ${{ always() }}
     steps:
-    - if: contains(needs.*.result, 'failure')
+    - if: contains(needs.*.result, 'failure') ||  contains(needs.*.result, 'cancelled')
       uses: actions/github-script@v7
       with:
         script: |

.github/workflows/nix-ci.yml

@@ -77,13 +77,7 @@ jobs:
           nix build $NIX_BUILD_ARGS .#cacheRoots -o push-build
       - name: Test
         run: |
-          nix build --keep-failed $NIX_BUILD_ARGS .#test -o push-test || (ln -s /tmp/nix-build-*/source/src/build/ ./push-test; false)
-      - name: Test Summary
-        uses: test-summary/action@v2
-        with:
-          paths: push-test/test-results.xml
-        if: always()
-        continue-on-error: true
+          nix build $NIX_BUILD_ARGS .#test -o push-test
       - name: Build manual
         run: |
           nix build $NIX_BUILD_ARGS --update-input lean --no-write-lock-file ./doc#{lean-mdbook,leanInk,alectryon,test,inked} -o push-doc

.github/workflows/pr-release.yml

@@ -126,19 +126,21 @@ jobs:
           if [ "$NIGHTLY_SHA" = "$MERGE_BASE_SHA" ]; then
             echo "The merge base of this PR coincides with the nightly release"
 
-            STD_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover/std4.git nightly-testing-"$MOST_RECENT_NIGHTLY")"
             MATHLIB_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover-community/mathlib4.git nightly-testing-"$MOST_RECENT_NIGHTLY")"
 
+            if [[ -n "$MATHLIB_REMOTE_TAGS" ]]; then
+              echo "... and Mathlib has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
+              MESSAGE=""
+            else
+              echo "... but Mathlib does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
+              MESSAGE="- ❗ Mathlib CI can not be attempted yet, as the \`nightly-testing-$MOST_RECENT_NIGHTLY\` tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto \`nightly-with-mathlib\`, Mathlib CI should run now."
+            fi
+
+            STD_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover/std4.git nightly-testing-"$MOST_RECENT_NIGHTLY")"
+
             if [[ -n "$STD_REMOTE_TAGS" ]]; then
               echo "... and Std has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
               MESSAGE=""
-
-              if [[ -n "$MATHLIB_REMOTE_TAGS" ]]; then
-                echo "... and Mathlib has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."    
-              else
-                echo "... but Mathlib does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
-                MESSAGE="- ❗ Mathlib CI can not be attempted yet, as the \`nightly-testing-$MOST_RECENT_NIGHTLY\` tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto \`nightly-with-mathlib\`, Mathlib CI should run now."
-              fi
             else
               echo "... but Std does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
               MESSAGE="- ❗ Std CI can not be attempted yet, as the \`nightly-testing-$MOST_RECENT_NIGHTLY\` tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto \`nightly-with-mathlib\`, Std CI should run now."
@@ -149,9 +151,7 @@ jobs:
             echo "but 'git merge-base origin/master HEAD' reported: $MERGE_BASE_SHA"
             git -C lean4.git log -10 origin/master
 
-            git -C lean4.git fetch origin nightly-with-mathlib 
-            NIGHTLY_WITH_MATHLIB_SHA="$(git -C lean4.git rev-parse "nightly-with-mathlib")"
-            MESSAGE="- ❗ Std/Mathlib CI will not be attempted unless your PR branches off the \`nightly-with-mathlib\` branch. Try \`git rebase $MERGE_BASE_SHA --onto $NIGHTLY_WITH_MATHLIB_SHA\`."
+            MESSAGE="- ❗ Std/Mathlib CI will not be attempted unless your PR branches off the \`nightly-with-mathlib\` branch. Try \`git rebase $MERGE_BASE_SHA --onto $NIGHTLY_SHA\`."
           fi
 
           if [[ -n "$MESSAGE" ]]; then

CMakeLists.txt

@@ -78,10 +78,6 @@ add_custom_target(update-stage0
   COMMAND $(MAKE) -C stage1 update-stage0
   DEPENDS stage1)
 
-add_custom_target(update-stage0-commit
-  COMMAND $(MAKE) -C stage1 update-stage0-commit
-  DEPENDS stage1)
-
 add_custom_target(test
   COMMAND $(MAKE) -C stage1 test
   DEPENDS stage1)

CODEOWNERS

@@ -13,7 +13,6 @@
 /src/Lean/Data/Lsp/ @mhuisi
 /src/Lean/Elab/Deriving/ @semorrison
 /src/Lean/Elab/Tactic/ @semorrison
-/src/Lean/Language/ @Kha
 /src/Lean/Meta/Tactic/ @leodemoura
 /src/Lean/Parser/ @Kha
 /src/Lean/PrettyPrinter/ @Kha

RELEASES.md

@@ -11,26 +11,21 @@ of each version.
 v4.8.0 (development in progress)
 ---------
 
-* **Executables configured with `supportInterpreter := true` on Windows should now be run via `lake exe` to function properly.**
-
-  The way Lean is built on Windows has changed (see PR [#3601](https://github.com/leanprover/lean4/pull/3601)). As a result, Lake now dynamically links executables with `supportInterpreter := true` on Windows to `libleanshared.dll` and `libInit_shared.dll`. Therefore, such executables will not run unless those shared libraries are co-located with the executables or part of `PATH`. Running the executable via `lake exe` will ensure these libraries are part of `PATH`.
-
-  In a related change, the signature of the `nativeFacets` Lake configuration options has changed from a static `Array` to a function `(shouldExport : Bool) → Array`. See its docstring or Lake's [README](src/lake/README.md) for further details on the changed option.
-
 * Lean now generates an error if the type of a theorem is **not** a proposition.
 
 * Importing two different files containing proofs of the same theorem is no longer considered an error. This feature is particularly useful for theorems that are automatically generated on demand (e.g., equational theorems).
 
-* Funcitonal induction principles.
+* New command `derive_functinal_induction`:
 
-  Derived from the definition of a (possibly mutually) recursive function, a **functional induction principle** is created that is tailored to proofs about that function.
-
-  For example from:
+  Derived from the definition of a (possibly mutually) recursive function
+  defined by well-founded recursion, a **functional induction principle** is
+  tailored to proofs about that function. For example from:
   ```
   def ackermann : Nat → Nat → Nat
     | 0, m => m + 1
     | n+1, 0 => ackermann n 1
     | n+1, m+1 => ackermann n (ackermann (n + 1) m)
+  derive_functional_induction ackermann
   ```
   we get
   ```
@@ -40,49 +35,6 @@ v4.8.0 (development in progress)
     (x x : Nat) : motive x x
   ```
 
-  It can be used in the `induction` tactic using the `using` syntax:
-  ```
-  induction n, m using ackermann.induct
-  ```
-
-* The termination checker now recognizes more recursion patterns without an
-  explicit `termination_by`. In particular the idiom of counting up to an upper
-  bound, as in
-  ```
-  def Array.sum (arr : Array Nat) (i acc : Nat) : Nat :=
-    if _ : i < arr.size then
-      Array.sum arr (i+1) (acc + arr[i])
-    else
-      acc
-  ```
-  is recognized without having to say `termination_by arr.size - i`.
-
-* Attribute `@[pp_using_anonymous_constructor]` to make structures pretty print like `⟨x, y, z⟩`
-  rather than `{a := x, b := y, c := z}`.
-  This attribute is applied to `Sigma`, `PSigma`, `PProd`, `Subtype`, `And`, and `Fin`.
-
-* Now structure instances pretty print with parent structures' fields inlined.
-  That is, if `B` extends `A`, then `{ toA := { x := 1 }, y := 2 }` now pretty prints as `{ x := 1, y := 2 }`.
-  Setting option `pp.structureInstances.flatten` to false turns this off.
-
-* Option `pp.structureProjections` is renamed to `pp.fieldNotation`, and there is now a suboption `pp.fieldNotation.generalized`
-  to enable pretty printing function applications using generalized field notation (defaults to true).
-  Field notation can be disabled on a function-by-function basis using the `@[pp_nodot]` attribute.
-
-* Added options `pp.mvars` (default: true) and `pp.mvars.withType` (default: false).
-  When `pp.mvars` is false, metavariables pretty print as `?_`,
-  and when `pp.mvars.withType` is true, metavariables pretty print with a type ascription.
-  These can be set when using `#guard_msgs` to make tests not rely on the unique ids assigned to anonymous metavariables.
-  [#3798](https://github.com/leanprover/lean4/pull/3798).
-
-* Added `@[induction_eliminator]` and `@[cases_eliminator]` attributes to be able to define custom eliminators
-  for the `induction` and `cases` tactics, replacing the `@[eliminator]` attribute.
-  Gives custom eliminators for `Nat` so that `induction` and `cases` put goal states into terms of `0` and `n + 1`
-  rather than `Nat.zero` and `Nat.succ n`.
-  Added option `tactic.customEliminators` to control whether to use custom eliminators.
-  [#3629](https://github.com/leanprover/lean4/pull/3629) and
-  [#3655](https://github.com/leanprover/lean4/pull/3655).
-
 Breaking changes:
 
 * Automatically generated equational theorems are now named using suffix `.eq_<idx>` instead of `._eq_<idx>`, and `.def` instead of `._unfold`. Example:
@@ -110,8 +62,6 @@ fact.def :
 -/
 ```
 
-* The coercion from `String` to `Name` was removed. Previously, it was `Name.mkSimple`, which does not separate strings at dots, but experience showed that this is not always the desired coercion. For the previous behavior, manually insert a call to `Name.mkSimple`.
-
 v4.7.0
 ---------
 

default.nix

@@ -0,0 +1,9 @@
+# used for `nix-shell https://github.com/leanprover/lean4/archive/master.tar.gz -A nix`
+{ nix = (import ./shell.nix {}).nix; } //
+(import (
+  fetchTarball {
+    url = "https://github.com/edolstra/flake-compat/archive/c75e76f80c57784a6734356315b306140646ee84.tar.gz";
+    sha256 = "071aal00zp2m9knnhddgr2wqzlx6i6qa1263lv1y7bdn2w20h10h"; }
+) {
+  src =  ./.;
+}).defaultNix

doc/dev/bootstrap.md

@@ -81,8 +81,20 @@ or using Github CLI with
 gh workflow run update-stage0.yml
 ```
 
-Leaving stage0 updates to the CI automation is preferable, but should you need to do it locally, you can use `make update-stage0-commit` in `build/release` to update `stage0` from `stage1` or `make -C stageN update-stage0-commit` to update from another stage.
-This command will automatically stage the updated files and introduce a commit, so make sure to commit your work before that. Then coordinate with the admins to not squash your PR so that stage 0 updates are preserved as separate commits.
+Leaving stage0 updates to the CI automation is preferrable, but should you need
+to do it locally, you can use `make update-stage0` in `build/release`, to
+update `stage0` from `stage1`, `make -C stageN update-stage0` to update from
+another stage, or `nix run .#update-stage0-commit` to update using nix.
+
+Updates to `stage0` should be their own commits in the Git history. So should
+you have to include the stage0 update in your PR (rather than using above
+automation after merging changes), commit your work before running `make
+update-stage0`, commit the updated `stage0` compiler code with the commit
+message:
+```
+chore: update stage0
+```
+and coordinate with the admins to not squash your PR.
 
 ## Further Bootstrapping Complications
 

doc/flake.nix

@@ -27,7 +27,7 @@
         src = inputs.mdBook;
         cargoDeps = drv.cargoDeps.overrideAttrs (_: {
           inherit src;
-          outputHash = "sha256-CO3A9Kpp4sIvkT9X3p+GTidazk7Fn4jf0AP2PINN44A=";
+          outputHash = "sha256-1YlPS6cqgxE4fjy9G8pWrpP27YrrbCDnfeyIsX81ZNw=";
         });
         doCheck = false;
       });

doc/make/index.md

@@ -12,7 +12,7 @@ Platform-Specific Setup
 - [Windows (msys2)](msys2.md)
 - [Windows (WSL)](wsl.md)
 - [macOS (homebrew)](osx-10.9.md)
-- Linux/macOS/WSL via [Nix](https://nixos.org/nix/): Call `nix develop` in the project root. That's it.
+- Linux/macOS/WSL via [Nix](https://nixos.org/nix/): Call `nix-shell` in the project root. That's it.
 
 Generic Build Instructions
 --------------------------

flake.lock

@@ -1,31 +1,12 @@
 {
   "nodes": {
-    "flake-compat": {
-      "flake": false,
-      "locked": {
-        "lastModified": 1673956053,
-        "narHash": "sha256-4gtG9iQuiKITOjNQQeQIpoIB6b16fm+504Ch3sNKLd8=",
-        "owner": "edolstra",
-        "repo": "flake-compat",
-        "rev": "35bb57c0c8d8b62bbfd284272c928ceb64ddbde9",
-        "type": "github"
-      },
-      "original": {
-        "owner": "edolstra",
-        "repo": "flake-compat",
-        "type": "github"
-      }
-    },
     "flake-utils": {
-      "inputs": {
-        "systems": "systems"
-      },
       "locked": {
-        "lastModified": 1710146030,
-        "narHash": "sha256-SZ5L6eA7HJ/nmkzGG7/ISclqe6oZdOZTNoesiInkXPQ=",
+        "lastModified": 1656928814,
+        "narHash": "sha256-RIFfgBuKz6Hp89yRr7+NR5tzIAbn52h8vT6vXkYjZoM=",
         "owner": "numtide",
         "repo": "flake-utils",
-        "rev": "b1d9ab70662946ef0850d488da1c9019f3a9752a",
+        "rev": "7e2a3b3dfd9af950a856d66b0a7d01e3c18aa249",
         "type": "github"
       },
       "original": {
@@ -37,11 +18,11 @@
     "lean4-mode": {
       "flake": false,
       "locked": {
-        "lastModified": 1709737301,
-        "narHash": "sha256-uT9JN2kLNKJK9c/S/WxLjiHmwijq49EgLb+gJUSDpz0=",
+        "lastModified": 1676498134,
+        "narHash": "sha256-u3WvyKxOViZG53hkb8wd2/Og6muTecbh+NdflIgVeyk=",
         "owner": "leanprover",
         "repo": "lean4-mode",
-        "rev": "f1f24c15134dee3754b82c9d9924866fe6bc6b9f",
+        "rev": "2c6ef33f476fdf5eb5e4fa4fa023ba8b11372440",
         "type": "github"
       },
       "original": {
@@ -50,35 +31,34 @@
         "type": "github"
       }
     },
-    "libgit2": {
+    "lowdown-src": {
       "flake": false,
       "locked": {
-        "lastModified": 1697646580,
-        "narHash": "sha256-oX4Z3S9WtJlwvj0uH9HlYcWv+x1hqp8mhXl7HsLu2f0=",
-        "owner": "libgit2",
-        "repo": "libgit2",
-        "rev": "45fd9ed7ae1a9b74b957ef4f337bc3c8b3df01b5",
+        "lastModified": 1633514407,
+        "narHash": "sha256-Dw32tiMjdK9t3ETl5fzGrutQTzh2rufgZV4A/BbxuD4=",
+        "owner": "kristapsdz",
+        "repo": "lowdown",
+        "rev": "d2c2b44ff6c27b936ec27358a2653caaef8f73b8",
         "type": "github"
       },
       "original": {
-        "owner": "libgit2",
-        "repo": "libgit2",
+        "owner": "kristapsdz",
+        "repo": "lowdown",
         "type": "github"
       }
     },
     "nix": {
       "inputs": {
-        "flake-compat": "flake-compat",
-        "libgit2": "libgit2",
+        "lowdown-src": "lowdown-src",
         "nixpkgs": "nixpkgs",
         "nixpkgs-regression": "nixpkgs-regression"
       },
       "locked": {
-        "lastModified": 1711102798,
-        "narHash": "sha256-CXOIJr8byjolqG7eqCLa+Wfi7rah62VmLoqSXENaZnw=",
+        "lastModified": 1657097207,
+        "narHash": "sha256-SmeGmjWM3fEed3kQjqIAO8VpGmkC2sL1aPE7kKpK650=",
         "owner": "NixOS",
         "repo": "nix",
-        "rev": "a22328066416650471c3545b0b138669ea212ab4",
+        "rev": "f6316b49a0c37172bca87ede6ea8144d7d89832f",
         "type": "github"
       },
       "original": {
@@ -89,33 +69,16 @@
     },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1709083642,
-        "narHash": "sha256-7kkJQd4rZ+vFrzWu8sTRtta5D1kBG0LSRYAfhtmMlSo=",
+        "lastModified": 1653988320,
+        "narHash": "sha256-ZaqFFsSDipZ6KVqriwM34T739+KLYJvNmCWzErjAg7c=",
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "b550fe4b4776908ac2a861124307045f8e717c8e",
+        "rev": "2fa57ed190fd6c7c746319444f34b5917666e5c1",
         "type": "github"
       },
       "original": {
         "owner": "NixOS",
-        "ref": "release-23.11",
-        "repo": "nixpkgs",
-        "type": "github"
-      }
-    },
-    "nixpkgs-old": {
-      "flake": false,
-      "locked": {
-        "lastModified": 1581379743,
-        "narHash": "sha256-i1XCn9rKuLjvCdu2UeXKzGLF6IuQePQKFt4hEKRU5oc=",
-        "owner": "NixOS",
-        "repo": "nixpkgs",
-        "rev": "34c7eb7545d155cc5b6f499b23a7cb1c96ab4d59",
-        "type": "github"
-      },
-      "original": {
-        "owner": "NixOS",
-        "ref": "nixos-19.03",
+        "ref": "nixos-22.05-small",
         "repo": "nixpkgs",
         "type": "github"
       }
@@ -138,11 +101,11 @@
     },
     "nixpkgs_2": {
       "locked": {
-        "lastModified": 1710889954,
-        "narHash": "sha256-Pr6F5Pmd7JnNEMHHmspZ0qVqIBVxyZ13ik1pJtm2QXk=",
+        "lastModified": 1686089707,
+        "narHash": "sha256-LTNlJcru2qJ0XhlhG9Acp5KyjB774Pza3tRH0pKIb3o=",
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "7872526e9c5332274ea5932a0c3270d6e4724f3b",
+        "rev": "af21c31b2a1ec5d361ed8050edd0303c31306397",
         "type": "github"
       },
       "original": {
@@ -157,23 +120,7 @@
         "flake-utils": "flake-utils",
         "lean4-mode": "lean4-mode",
         "nix": "nix",
-        "nixpkgs": "nixpkgs_2",
-        "nixpkgs-old": "nixpkgs-old"
-      }
-    },
-    "systems": {
-      "locked": {
-        "lastModified": 1681028828,
-        "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
-        "owner": "nix-systems",
-        "repo": "default",
-        "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e",
-        "type": "github"
-      },
-      "original": {
-        "owner": "nix-systems",
-        "repo": "default",
-        "type": "github"
+        "nixpkgs": "nixpkgs_2"
       }
     }
   },

flake.nix

@@ -2,9 +2,6 @@
   description = "Lean interactive theorem prover";
 
   inputs.nixpkgs.url = "github:NixOS/nixpkgs/nixpkgs-unstable";
-  # old nixpkgs used for portable release with older glibc (2.27)
-  inputs.nixpkgs-old.url = "github:NixOS/nixpkgs/nixos-19.03";
-  inputs.nixpkgs-old.flake = false;
   inputs.flake-utils.url = "github:numtide/flake-utils";
   inputs.nix.url = "github:NixOS/nix";
   inputs.lean4-mode = {
@@ -20,41 +17,14 @@
   #  inputs.lean4-mode.follows = "lean4-mode";
   #};
 
-  outputs = { self, nixpkgs, nixpkgs-old, flake-utils, nix, lean4-mode, ... }@inputs: flake-utils.lib.eachDefaultSystem (system:
+  outputs = { self, nixpkgs, flake-utils, nix, lean4-mode, ... }@inputs: flake-utils.lib.eachDefaultSystem (system:
     let
       pkgs = import nixpkgs {
         inherit system;
         # for `vscode-with-extensions`
         config.allowUnfree = true;
       };
-      # An old nixpkgs for creating releases with an old glibc
-      pkgsDist-old = import nixpkgs-old { inherit system; };
-      # An old nixpkgs for creating releases with an old glibc
-      pkgsDist-old-aarch = import nixpkgs-old { localSystem.config = "aarch64-unknown-linux-gnu"; };
-
       lean-packages = pkgs.callPackage (./nix/packages.nix) { src = ./.; inherit nix lean4-mode; };
-
-      devShellWithDist = pkgsDist: pkgs.mkShell.override {
-	  stdenv = pkgs.overrideCC pkgs.stdenv lean-packages.llvmPackages.clang;
-	} ({
-	  buildInputs = with pkgs; [
-	    cmake gmp ccache
-	    lean-packages.llvmPackages.llvm  # llvm-symbolizer for asan/lsan
-	    # TODO: only add when proven to not affect the flakification
-	    #pkgs.python3
-	  ];
-	  # https://github.com/NixOS/nixpkgs/issues/60919
-	  hardeningDisable = [ "all" ];
-	  # more convenient `ctest` output
-	  CTEST_OUTPUT_ON_FAILURE = 1;
-	} // pkgs.lib.optionalAttrs pkgs.stdenv.isLinux {
-	  GMP = pkgsDist.gmp.override { withStatic = true; };
-	  GLIBC = pkgsDist.glibc;
-	  GLIBC_DEV = pkgsDist.glibc.dev;
-	  GCC_LIB = pkgsDist.gcc.cc.lib;
-	  ZLIB = pkgsDist.zlib;
-	  GDB = pkgsDist.gdb;
-	});
     in {
       packages = lean-packages // rec {
         debug = lean-packages.override { debug = true; };
@@ -79,10 +49,7 @@
       };
       defaultPackage = lean-packages.lean-all;
 
-      # The default development shell for working on lean itself
-      devShells.default = devShellWithDist pkgs;
-      devShells.oldGlibc = devShellWithDist pkgsDist-old;
-      devShells.oldGlibcAArch = devShellWithDist pkgsDist-old-aarch;
+      inherit (lean-packages) devShell;
 
       checks.lean = lean-packages.test;
     }) // rec {

nix/bootstrap.nix

@@ -65,7 +65,7 @@ rec {
     installPhase = ''
       mkdir -p $out/bin $out/lib/lean
       mv bin/lean $out/bin/
-      mv lib/lean/*.{so,dylib} $out/lib/lean
+      mv lib/lean/*.so $out/lib/lean
     '';
     meta.mainProgram = "lean";
   });
@@ -170,11 +170,10 @@ rec {
           ln -sf ${lean-all}/* .
         '';
         buildPhase = ''
-          ctest --output-junit test-results.xml --output-on-failure -E 'leancomptest_(doc_example|foreign)' -j$NIX_BUILD_CORES
+          ctest --output-on-failure -E 'leancomptest_(doc_example|foreign)' -j$NIX_BUILD_CORES
         '';
         installPhase = ''
-          mkdir $out
-          mv test-results.xml $out
+          touch $out
         '';
       };
       update-stage0 =

nix/buildLeanPackage.nix

@@ -176,7 +176,7 @@ with builtins; let
       # make local "copy" so `drv`'s Nix store path doesn't end up in ccache's hash
       ln -s ${drv.c}/${drv.cPath} src.c
       # on the other hand, a debug build is pretty fast anyway, so preserve the path for gdb
-      leanc -c -o $out/$oPath $leancFlags -fPIC ${if debug then "${drv.c}/${drv.cPath} -g" else "src.c -O3 -DNDEBUG -DLEAN_EXPORTING"}
+      leanc -c -o $out/$oPath $leancFlags -fPIC ${if debug then "${drv.c}/${drv.cPath} -g" else "src.c -O3 -DNDEBUG"}
     '';
   };
   mkMod = mod: deps:

shell.nix

@@ -0,0 +1,27 @@
+let
+  flake = (import ./default.nix);
+  flakePkgs = flake.packages.${builtins.currentSystem};
+in { pkgs ? flakePkgs.nixpkgs, pkgsDist ? pkgs }:
+# use `shell` as default
+(attribs: attribs.shell // attribs) rec {
+  shell = pkgs.mkShell.override {
+    stdenv = pkgs.overrideCC pkgs.stdenv flakePkgs.llvmPackages.clang;
+  } (rec {
+    buildInputs = with pkgs; [
+      cmake gmp ccache
+      flakePkgs.llvmPackages.llvm  # llvm-symbolizer for asan/lsan
+    ];
+    # https://github.com/NixOS/nixpkgs/issues/60919
+    hardeningDisable = [ "all" ];
+    # more convenient `ctest` output
+    CTEST_OUTPUT_ON_FAILURE = 1;
+  } // pkgs.lib.optionalAttrs pkgs.stdenv.isLinux {
+    GMP = pkgsDist.gmp.override { withStatic = true; };
+    GLIBC = pkgsDist.glibc;
+    GLIBC_DEV = pkgsDist.glibc.dev;
+    GCC_LIB = pkgsDist.gcc.cc.lib;
+    ZLIB = pkgsDist.zlib;
+    GDB = pkgsDist.gdb;
+  });
+  nix = flake.devShell.${builtins.currentSystem};
+}

src/CMakeLists.txt

@@ -503,13 +503,13 @@ file(RELATIVE_PATH LIB ${LEAN_SOURCE_DIR} ${CMAKE_BINARY_DIR}/lib)
 
 # set up libInit_shared only on Windows; see also stdlib.make.in
 if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
-  set(INIT_SHARED_LINKER_FLAGS "-Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/temp/libInit.a.export ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a -Wl,--no-whole-archive -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libInit_shared.dll.a")
+  set(INIT_SHARED_LINKER_FLAGS "-Wl,--whole-archive -lInit ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a -Wl,--no-whole-archive -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libInit_shared.dll.a")
 endif()
 
 if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
   set(LEANSHARED_LINKER_FLAGS "-Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libInit.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libLean.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libleancpp.a ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS}")
 elseif(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
-  set(LEANSHARED_LINKER_FLAGS "-Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/temp/libLean.a.export -lleancpp -Wl,--no-whole-archive -lInit_shared -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libleanshared.dll.a")
+  set(LEANSHARED_LINKER_FLAGS "-Wl,--whole-archive -lLean -lleancpp -Wl,--no-whole-archive -lInit_shared -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libleanshared.dll.a")
 else()
   set(LEANSHARED_LINKER_FLAGS "-Wl,--whole-archive -lInit -lLean -lleancpp -Wl,--no-whole-archive ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS}")
 endif()
@@ -588,10 +588,6 @@ if(PREV_STAGE)
     COMMAND bash -c 'CSRCS=${CMAKE_BINARY_DIR}/lib/temp script/update-stage0'
     DEPENDS make_stdlib
     WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/..")
-
-  add_custom_target(update-stage0-commit
-    COMMAND git commit -m "chore: update stage0"
-    DEPENDS update-stage0)
 endif()
 
 # use Bash version for building, use Lean version in bin/ for tests & distribution

src/Init.lean

@@ -33,4 +33,3 @@ import Init.SizeOfLemmas
 import Init.BinderPredicates
 import Init.Ext
 import Init.Omega
-import Init.MacroTrace

src/Init/ByCases.lean

@@ -21,9 +21,9 @@ macro_rules
 
 /-! ## if-then-else -/
 
-@[simp] theorem if_true {_ : Decidable True} (t e : α) : ite True t e = t := if_pos trivial
+@[simp] theorem if_true {h : Decidable True} (t e : α) : ite True t e = t := if_pos trivial
 
-@[simp] theorem if_false {_ : Decidable False} (t e : α) : ite False t e = e := if_neg id
+@[simp] theorem if_false {h : Decidable False} (t e : α) : ite False t e = e := if_neg id
 
 theorem ite_id [Decidable c] {α} (t : α) : (if c then t else t) = t := by split <;> rfl
 

src/Init/Control/ExceptCps.lean

@@ -18,7 +18,6 @@ namespace ExceptCpsT
 def run {ε α : Type u} [Monad m] (x : ExceptCpsT ε m α) : m (Except ε α) :=
   x _ (fun a => pure (Except.ok a)) (fun e => pure (Except.error e))
 
-set_option linter.unusedVariables false in  -- `s` unused
 @[always_inline, inline]
 def runK {ε α : Type u} (x : ExceptCpsT ε m α) (s : ε) (ok : α → m β) (error : ε → m β) : m β :=
   x _ ok error

src/Init/Conv.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 Notation for operators defined at Prelude.lean
 -/
 prelude
-import Init.Tactics
+import Init.Meta
 
 namespace Lean.Parser.Tactic.Conv
 
@@ -201,7 +201,7 @@ macro (name := anyGoals) tk:"any_goals " s:convSeq : conv =>
   with inaccessible names to the given names.
 * `case tag₁ | tag₂ => tac` is equivalent to `(case tag₁ => tac); (case tag₂ => tac)`.
 -/
-macro (name := case) tk:"case " args:sepBy1(caseArg, "|") arr:" => " s:convSeq : conv =>
+macro (name := case) tk:"case " args:sepBy1(caseArg, " | ") arr:" => " s:convSeq : conv =>
   `(conv| tactic' => case%$tk $args|* =>%$arr conv' => ($s); all_goals rfl)
 
 /--
@@ -210,7 +210,7 @@ has been solved after applying `tac`, nor admits the goal if `tac` failed.
 Recall that `case` closes the goal using `sorry` when `tac` fails, and
 the tactic execution is not interrupted.
 -/
-macro (name := case') tk:"case' " args:sepBy1(caseArg, "|") arr:" => " s:convSeq : conv =>
+macro (name := case') tk:"case' " args:sepBy1(caseArg, " | ") arr:" => " s:convSeq : conv =>
   `(conv| tactic' => case'%$tk $args|* =>%$arr conv' => $s)
 
 /--

src/Init/Core.lean

@@ -19,7 +19,7 @@ which applies to all applications of the function).
 -/
 @[simp] def inline {α : Sort u} (a : α) : α := a
 
-theorem id_def {α : Sort u} (a : α) : id a = a := rfl
+theorem id.def {α : Sort u} (a : α) : id a = a := rfl
 
 /--
 `flip f a b` is `f b a`. It is useful for "point-free" programming,
@@ -165,7 +165,6 @@ whose first component is `a : α` and whose second component is `b : β a`
 It is sometimes known as the dependent sum type, since it is the type level version
 of an indexed summation.
 -/
-@[pp_using_anonymous_constructor]
 structure Sigma {α : Type u} (β : α → Type v) where
   /-- Constructor for a dependent pair. If `a : α` and `b : β a` then `⟨a, b⟩ : Sigma β`.
   (This will usually require a type ascription to determine `β`
@@ -191,7 +190,6 @@ which can cause problems for universe level unification,
 because the equation `max 1 u v = ?u + 1` has no solution in level arithmetic.
 `PSigma` is usually only used in automation that constructs pairs of arbitrary types.
 -/
-@[pp_using_anonymous_constructor]
 structure PSigma {α : Sort u} (β : α → Sort v) where
   /-- Constructor for a dependent pair. If `a : α` and `b : β a` then `⟨a, b⟩ : PSigma β`.
   (This will usually require a type ascription to determine `β`
@@ -1308,6 +1306,7 @@ gen_injective_theorems% Fin
 gen_injective_theorems% Array
 gen_injective_theorems% Sum
 gen_injective_theorems% PSum
+gen_injective_theorems% Nat
 gen_injective_theorems% Option
 gen_injective_theorems% List
 gen_injective_theorems% Except
@@ -1315,12 +1314,6 @@ gen_injective_theorems% EStateM.Result
 gen_injective_theorems% Lean.Name
 gen_injective_theorems% Lean.Syntax
 
-theorem Nat.succ.inj {m n : Nat} : m.succ = n.succ → m = n :=
-  fun x => Nat.noConfusion x id
-
-theorem Nat.succ.injEq (u v : Nat) : (u.succ = v.succ) = (u = v) :=
-  Eq.propIntro Nat.succ.inj (congrArg Nat.succ)
-
 @[simp] theorem beq_iff_eq [BEq α] [LawfulBEq α] (a b : α) : a == b ↔ a = b :=
   ⟨eq_of_beq, by intro h; subst h; exact LawfulBEq.rfl⟩
 
@@ -1601,7 +1594,7 @@ protected def mk' {α : Sort u} [s : Setoid α] (a : α) : Quotient s :=
 The analogue of `Quot.sound`: If `a` and `b` are related by the equivalence relation,
 then they have equal equivalence classes.
 -/
-theorem sound {α : Sort u} {s : Setoid α} {a b : α} : a ≈ b → Quotient.mk s a = Quotient.mk s b :=
+def sound {α : Sort u} {s : Setoid α} {a b : α} : a ≈ b → Quotient.mk s a = Quotient.mk s b :=
   Quot.sound
 
 /--

src/Init/Data/Array/Basic.lean

@@ -10,7 +10,7 @@ import Init.Data.Fin.Basic
 import Init.Data.UInt.Basic
 import Init.Data.Repr
 import Init.Data.ToString.Basic
-import Init.GetElem
+import Init.Util
 universe u v w
 
 namespace Array
@@ -59,8 +59,6 @@ def uget (a : @& Array α) (i : USize) (h : i.toNat < a.size) : α :=
 instance : GetElem (Array α) USize α fun xs i => i.toNat < xs.size where
   getElem xs i h := xs.uget i h
 
-instance : LawfulGetElem (Array α) USize α fun xs i => i.toNat < xs.size where
-
 def back [Inhabited α] (a : Array α) : α :=
   a.get! (a.size - 1)
 
@@ -458,12 +456,24 @@ def findRev? {α : Type} (as : Array α) (p : α → Bool) : Option α :=
 
 @[inline]
 def findIdx? {α : Type u} (as : Array α) (p : α → Bool) : Option Nat :=
-  let rec loop (j : Nat) :=
-    if h : j < as.size then
-      if p as[j] then some j else loop (j + 1)
-    else none
-    termination_by as.size - j
-  loop 0
+  let rec loop (i : Nat) (j : Nat) (inv : i + j = as.size) : Option Nat :=
+    if hlt : j < as.size then
+      match i, inv with
+      | 0, inv => by
+        apply False.elim
+        rw [Nat.zero_add] at inv
+        rw [inv] at hlt
+        exact absurd hlt (Nat.lt_irrefl _)
+      | i+1, inv =>
+        if p as[j] then
+          some j
+        else
+          have : i + (j+1) = as.size := by
+            rw [← inv, Nat.add_comm j 1, Nat.add_assoc]
+          loop i (j+1) this
+    else
+      none
+  loop as.size 0 rfl
 
 def getIdx? [BEq α] (a : Array α) (v : α) : Option Nat :=
 a.findIdx? fun a => a == v
@@ -717,36 +727,33 @@ def takeWhile (p : α → Bool) (as : Array α) : Array α :=
     termination_by as.size - i
   go 0 #[]
 
-/-- Remove the element at a given index from an array without bounds checks, using a `Fin` index.
-
-  This function takes worst case O(n) time because
-  it has to backshift all elements at positions greater than `i`.-/
-def feraseIdx (a : Array α) (i : Fin a.size) : Array α :=
-  if h : i.val + 1 < a.size then
-    let a' := a.swap ⟨i.val + 1, h⟩ i
-    let i' : Fin a'.size := ⟨i.val + 1, by simp [a', h]⟩
-    have : a'.size - i' < a.size - i := by
-      simp [a', Nat.sub_succ_lt_self _ _ i.isLt]
-    a'.feraseIdx i'
+def eraseIdxAux (i : Nat) (a : Array α) : Array α :=
+  if h : i < a.size then
+    let idx  : Fin a.size := ⟨i, h⟩;
+    let idx1 : Fin a.size := ⟨i - 1, by exact Nat.lt_of_le_of_lt (Nat.pred_le i) h⟩;
+    let a' := a.swap idx idx1
+    eraseIdxAux (i+1) a'
   else
     a.pop
-termination_by a.size - i.val
+termination_by a.size - i
 
-theorem size_feraseIdx (a : Array α) (i : Fin a.size) : (a.feraseIdx i).size = a.size - 1 := by
-  induction a, i using Array.feraseIdx.induct with
-  | @case1 a i h a' _ _ ih =>
-    unfold feraseIdx
-    simp [h, a', ih]
-  | case2 a i h =>
-    unfold feraseIdx
-    simp [h]
+def feraseIdx (a : Array α) (i : Fin a.size) : Array α :=
+  eraseIdxAux (i.val + 1) a
 
-/-- Remove the element at a given index from an array, or do nothing if the index is out of bounds.
-
-  This function takes worst case O(n) time because
-  it has to backshift all elements at positions greater than `i`.-/
 def eraseIdx (a : Array α) (i : Nat) : Array α :=
-  if h : i < a.size then a.feraseIdx ⟨i, h⟩ else a
+  if i < a.size then eraseIdxAux (i+1) a else a
+
+def eraseIdxSzAux (a : Array α) (i : Nat) (r : Array α) (heq : r.size = a.size) : { r : Array α // r.size = a.size - 1 } :=
+  if h : i < r.size then
+    let idx  : Fin r.size := ⟨i, h⟩;
+    let idx1 : Fin r.size := ⟨i - 1, by exact Nat.lt_of_le_of_lt (Nat.pred_le i) h⟩;
+    eraseIdxSzAux a (i+1) (r.swap idx idx1) ((size_swap r idx idx1).trans heq)
+  else
+    ⟨r.pop, (size_pop r).trans (heq ▸ rfl)⟩
+termination_by r.size - i
+
+def eraseIdx' (a : Array α) (i : Fin a.size) : { r : Array α // r.size = a.size - 1 } :=
+  eraseIdxSzAux a (i.val + 1) a rfl
 
 def erase [BEq α] (as : Array α) (a : α) : Array α :=
   match as.indexOf? a with

src/Init/Data/Array/Subarray.lean

@@ -32,8 +32,6 @@ def get (s : Subarray α) (i : Fin s.size) : α :=
 instance : GetElem (Subarray α) Nat α fun xs i => i < xs.size where
   getElem xs i h := xs.get ⟨i, h⟩
 
-instance : LawfulGetElem (Subarray α) Nat α fun xs i => i < xs.size where
-
 @[inline] def getD (s : Subarray α) (i : Nat) (v₀ : α) : α :=
   if h : i < s.size then s.get ⟨i, h⟩ else v₀
 

src/Init/Data/BitVec/Basic.lean

@@ -618,14 +618,4 @@ section normalization_eqs
 @[simp] theorem zero_eq                                   : BitVec.zero n = 0#n               := rfl
 end normalization_eqs
 
-/-- Converts a list of `Bool`s to a big-endian `BitVec`. -/
-def ofBoolListBE : (bs : List Bool) → BitVec bs.length
-| [] => 0#0
-| b :: bs => cons b (ofBoolListBE bs)
-
-/-- Converts a list of `Bool`s to a little-endian `BitVec`. -/
-def ofBoolListLE : (bs : List Bool) → BitVec bs.length
-| [] => 0#0
-| b :: bs => concat (ofBoolListLE bs) b
-
 end BitVec

src/Init/Data/BitVec/Lemmas.lean

@@ -41,36 +41,12 @@ theorem testBit_toNat (x : BitVec w) : x.toNat.testBit i = x.getLsb i := rfl
   have p : 2^w ≤ 2^i := Nat.pow_le_pow_of_le_right (by omega) ge
   omega
 
-@[simp] theorem getMsb_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : getMsb x i = false := by
-  rw [getMsb]
-  simp only [Bool.and_eq_false_imp, decide_eq_true_eq]
-  omega
-
 theorem lt_of_getLsb (x : BitVec w) (i : Nat) : getLsb x i = true → i < w := by
   if h : i < w then
     simp [h]
   else
     simp [Nat.ge_of_not_lt h]
 
-theorem lt_of_getMsb (x : BitVec w) (i : Nat) : getMsb x i = true → i < w := by
-  if h : i < w then
-    simp [h]
-  else
-    simp [Nat.ge_of_not_lt h]
-
-theorem getMsb_eq_getLsb (x : BitVec w) (i : Nat) : x.getMsb i = (decide (i < w) && x.getLsb (w - 1 - i)) := by
-  rw [getMsb]
-
-theorem getLsb_eq_getMsb (x : BitVec w) (i : Nat) : x.getLsb i = (decide (i < w) && x.getMsb (w - 1 - i)) := by
-  rw [getMsb]
-  by_cases h₁ : i < w <;> by_cases h₂ : w - 1 - i < w <;>
-    simp only [h₁, h₂] <;> simp only [decide_True, decide_False, Bool.false_and, Bool.and_false, Bool.true_and, Bool.and_true]
-  · congr
-    omega
-  all_goals
-    apply getLsb_ge
-    omega
-
 -- We choose `eq_of_getLsb_eq` as the `@[ext]` theorem for `BitVec`
 -- somewhat arbitrarily over `eq_of_getMsg_eq`.
 @[ext] theorem eq_of_getLsb_eq {x y : BitVec w}
@@ -120,8 +96,6 @@ theorem ofNat_one (n : Nat) : BitVec.ofNat 1 n = BitVec.ofBool (n % 2 = 1) :=  b
 theorem ofBool_eq_iff_eq : ∀(b b' : Bool), BitVec.ofBool b = BitVec.ofBool b' ↔ b = b' := by
   decide
 
-@[simp] theorem not_ofBool : ~~~ (ofBool b) = ofBool (!b) := by cases b <;> rfl
-
 @[simp, bv_toNat] theorem toNat_ofFin (x : Fin (2^n)) : (BitVec.ofFin x).toNat = x.val := rfl
 
 @[simp] theorem toNat_ofNatLt (x : Nat) (p : x < 2^w) : (x#'p).toNat = x := rfl
@@ -316,19 +290,6 @@ theorem nat_eq_toNat (x : BitVec w) (y : Nat)
     getLsb (zeroExtend' ge x) i = getLsb x i := by
   simp [getLsb, toNat_zeroExtend']
 
-@[simp] theorem getMsb_zeroExtend' (ge : m ≥ n) (x : BitVec n) (i : Nat) :
-    getMsb (zeroExtend' ge x) i = (decide (i ≥ m - n) && getMsb x (i - (m - n))) := by
-  simp only [getMsb, getLsb_zeroExtend', gt_iff_lt]
-  by_cases h₁ : decide (i < m) <;> by_cases h₂ : decide (i ≥ m - n) <;> by_cases h₃ : decide (i - (m - n) < n) <;>
-    by_cases h₄ : n - 1 - (i - (m - n)) = m - 1 - i
-  all_goals
-    simp only [h₁, h₂, h₃, h₄]
-    simp_all only [ge_iff_le, decide_eq_true_eq, Nat.not_le, Nat.not_lt, Bool.true_and,
-      Bool.false_and, Bool.and_self] <;>
-    (try apply getLsb_ge) <;>
-    (try apply (getLsb_ge _ _ _).symm) <;>
-    omega
-
 @[simp] theorem getLsb_zeroExtend (m : Nat) (x : BitVec n) (i : Nat) :
     getLsb (zeroExtend m x) i = (decide (i < m) && getLsb x i) := by
   simp [getLsb, toNat_zeroExtend, Nat.testBit_mod_two_pow]
@@ -519,24 +480,6 @@ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
   simp [h]
   omega
 
-/-! ### cast -/
-
-@[simp] theorem not_cast {x : BitVec w} (h : w = w') : ~~~(cast h x) = cast h (~~~x) := by
-  ext
-  simp_all [lt_of_getLsb]
-
-@[simp] theorem and_cast {x y : BitVec w} (h : w = w') : cast h x &&& cast h y = cast h (x &&& y) := by
-  ext
-  simp_all [lt_of_getLsb]
-
-@[simp] theorem or_cast {x y : BitVec w} (h : w = w') : cast h x ||| cast h y = cast h (x ||| y) := by
-  ext
-  simp_all [lt_of_getLsb]
-
-@[simp] theorem xor_cast {x y : BitVec w} (h : w = w') : cast h x &&& cast h y = cast h (x &&& y) := by
-  ext
-  simp_all [lt_of_getLsb]
-
 /-! ### shiftLeft -/
 
 @[simp, bv_toNat] theorem toNat_shiftLeft {x : BitVec v} :
@@ -586,11 +529,6 @@ theorem shiftLeftZeroExtend_eq {x : BitVec w} :
     <;> simp_all
     <;> (rw [getLsb_ge]; omega)
 
-@[simp] theorem getMsb_shiftLeftZeroExtend (x : BitVec m) (n : Nat) :
-    getMsb (shiftLeftZeroExtend x n) i = getMsb x i := by
-  have : n ≤ i + n := by omega
-  simp_all [shiftLeftZeroExtend_eq]
-
 @[simp] theorem msb_shiftLeftZeroExtend (x : BitVec w) (i : Nat) :
     (shiftLeftZeroExtend x i).msb = x.msb := by
   simp [shiftLeftZeroExtend_eq, BitVec.msb]
@@ -615,18 +553,11 @@ theorem append_def (x : BitVec v) (y : BitVec w) :
 
 @[simp] theorem getLsb_append {v : BitVec n} {w : BitVec m} :
     getLsb (v ++ w) i = bif i < m then getLsb w i else getLsb v (i - m) := by
-  simp only [append_def, getLsb_or, getLsb_shiftLeftZeroExtend, getLsb_zeroExtend']
+  simp [append_def]
   by_cases h : i < m
   · simp [h]
   · simp [h]; simp_all
 
-@[simp] theorem getMsb_append {v : BitVec n} {w : BitVec m} :
-    getMsb (v ++ w) i = bif n ≤ i then getMsb w (i - n) else getMsb v i := by
-  simp [append_def]
-  by_cases h : n ≤ i
-  · simp [h]
-  · simp [h]
-
 theorem msb_append {x : BitVec w} {y : BitVec v} :
     (x ++ y).msb = bif (w == 0) then (y.msb) else (x.msb) := by
   rw [← append_eq, append]
@@ -655,31 +586,6 @@ theorem msb_append {x : BitVec w} {y : BitVec v} :
 @[simp] theorem truncate_cons {x : BitVec w} : (cons a x).truncate w = x := by
   simp [cons]
 
-@[simp] theorem not_append {x : BitVec w} {y : BitVec v} : ~~~ (x ++ y) = (~~~ x) ++ (~~~ y) := by
-  ext i
-  simp only [getLsb_not, getLsb_append, cond_eq_if]
-  split
-  · simp_all
-  · simp_all; omega
-
-@[simp] theorem and_append {x₁ x₂ : BitVec w} {y₁ y₂ : BitVec v} :
-    (x₁ ++ y₁) &&& (x₂ ++ y₂) = (x₁ &&& x₂) ++ (y₁ &&& y₂) := by
-  ext i
-  simp only [getLsb_append, cond_eq_if]
-  split <;> simp [*]
-
-@[simp] theorem or_append {x₁ x₂ : BitVec w} {y₁ y₂ : BitVec v} :
-    (x₁ ++ y₁) ||| (x₂ ++ y₂) = (x₁ ||| x₂) ++ (y₁ ||| y₂) := by
-  ext i
-  simp only [getLsb_append, cond_eq_if]
-  split <;> simp [*]
-
-@[simp] theorem xor_append {x₁ x₂ : BitVec w} {y₁ y₂ : BitVec v} :
-    (x₁ ++ y₁) ^^^ (x₂ ++ y₂) = (x₁ ^^^ x₂) ++ (y₁ ^^^ y₂) := by
-  ext i
-  simp only [getLsb_append, cond_eq_if]
-  split <;> simp [*]
-
 /-! ### rev -/
 
 theorem getLsb_rev (x : BitVec w) (i : Fin w) :
@@ -724,12 +630,6 @@ theorem toNat_cons' {x : BitVec w} :
 @[simp] theorem msb_cons : (cons a x).msb = a := by
   simp [cons, msb_cast, msb_append]
 
-@[simp] theorem getMsb_cons_zero : (cons a x).getMsb 0 = a := by
-  rw [← BitVec.msb, msb_cons]
-
-@[simp] theorem getMsb_cons_succ : (cons a x).getMsb (i + 1) = x.getMsb i := by
-  simp [cons, Nat.le_add_left 1 i]
-
 theorem truncate_succ (x : BitVec w) :
     truncate (i+1) x = cons (getLsb x i) (truncate i x) := by
   apply eq_of_getLsb_eq
@@ -750,21 +650,6 @@ theorem eq_msb_cons_truncate (x : BitVec (w+1)) : x = (cons x.msb (x.truncate w)
     · simp_all
     · omega
 
-@[simp] theorem not_cons (x : BitVec w) (b : Bool) : ~~~(cons b x) = cons (!b) (~~~x) := by
-  simp [cons]
-
-@[simp] theorem cons_or_cons (x y : BitVec w) (a b : Bool) :
-    (cons a x) ||| (cons b y) = cons (a || b) (x ||| y) := by
-  ext i; cases i using Fin.succRecOn <;> simp <;> split <;> rfl
-
-@[simp] theorem cons_and_cons (x y : BitVec w) (a b : Bool) :
-    (cons a x) &&& (cons b y) = cons (a && b) (x &&& y) := by
-  ext i; cases i using Fin.succRecOn <;> simp <;> split <;> rfl
-
-@[simp] theorem cons_xor_cons (x y : BitVec w) (a b : Bool) :
-    (cons a x) ^^^ (cons b y) = cons (xor a b) (x ^^^ y) := by
-  ext i; cases i using Fin.succRecOn <;> simp <;> split <;> rfl
-
 /-! ### concat -/
 
 @[simp] theorem toNat_concat (x : BitVec w) (b : Bool) :
@@ -940,7 +825,7 @@ protected theorem lt_of_le_ne (x y : BitVec n) (h1 : x <= y) (h2 : ¬ x = y) : x
   simp
   exact Nat.lt_of_le_of_ne
 
-/-! ### intMax -/
+/- ! ### intMax -/
 
 /-- The bitvector of width `w` that has the largest value when interpreted as an integer. -/
 def intMax (w : Nat) : BitVec w  := (2^w - 1)#w
@@ -954,20 +839,4 @@ theorem toNat_intMax_eq : (intMax w).toNat = 2^w - 1 := by
     omega
   simp [intMax, Nat.shiftLeft_eq, Nat.one_mul, natCast_eq_ofNat, toNat_ofNat, Nat.mod_eq_of_lt h]
 
-/-! ### ofBoolList -/
-
-@[simp] theorem getMsb_ofBoolListBE : (ofBoolListBE bs).getMsb i = bs.getD i false := by
-  induction bs generalizing i <;> cases i <;> simp_all [ofBoolListBE]
-
-@[simp] theorem getLsb_ofBoolListBE :
-    (ofBoolListBE bs).getLsb i = (decide (i < bs.length) && bs.getD (bs.length - 1 - i) false) := by
-  simp [getLsb_eq_getMsb]
-
-@[simp] theorem getLsb_ofBoolListLE : (ofBoolListLE bs).getLsb i = bs.getD i false := by
-  induction bs generalizing i <;> cases i <;> simp_all [ofBoolListLE]
-
-@[simp] theorem getMsb_ofBoolListLE :
-    (ofBoolListLE bs).getMsb i = (decide (i < bs.length) && bs.getD (bs.length - 1 - i) false) := by
-  simp [getMsb_eq_getLsb]
-
 end BitVec

src/Init/Data/Bool.lean

@@ -220,12 +220,6 @@ due to `beq_iff_eq`.
 
 /-! ### coercision related normal forms -/
 
-theorem beq_eq_decide_eq [BEq α] [LawfulBEq α] [DecidableEq α] (a b : α) :
-    (a == b) = decide (a = b) := by
-  cases h : a == b
-  · simp [ne_of_beq_false h]
-  · simp [eq_of_beq h]
-
 @[simp] theorem not_eq_not : ∀ {a b : Bool}, ¬a = !b ↔ a = b := by decide
 
 @[simp] theorem not_not_eq : ∀ {a b : Bool}, ¬(!a) = b ↔ a = b := by decide
@@ -236,11 +230,6 @@ theorem beq_eq_decide_eq [BEq α] [LawfulBEq α] [DecidableEq α] (a b : α) :
 @[simp] theorem coe_false_iff_true  : ∀(a b : Bool), (a = false ↔ b) ↔ (!a) = b := by decide
 @[simp] theorem coe_false_iff_false : ∀(a b : Bool), (a = false ↔ b = false) ↔ (!a) = (!b) := by decide
 
-/-! ### beq properties -/
-
-theorem beq_comm {α} [BEq α] [LawfulBEq α] {a b : α} : (a == b) = (b == a) :=
-  (Bool.coe_iff_coe (a == b) (b == a)).mp (by simp [@eq_comm α])
-
 /-! ### xor -/
 
 theorem false_xor : ∀ (x : Bool), xor false x = x := false_bne

src/Init/Data/ByteArray/Basic.lean

@@ -52,13 +52,9 @@ def get : (a : @& ByteArray) → (@& Fin a.size) → UInt8
 instance : GetElem ByteArray Nat UInt8 fun xs i => i < xs.size where
   getElem xs i h := xs.get ⟨i, h⟩
 
-instance : LawfulGetElem ByteArray Nat UInt8 fun xs i => i < xs.size where
-
 instance : GetElem ByteArray USize UInt8 fun xs i => i.val < xs.size where
   getElem xs i h := xs.uget i h
 
-instance : LawfulGetElem ByteArray USize UInt8 fun xs i => i.val < xs.size where
-
 @[extern "lean_byte_array_set"]
 def set! : ByteArray → (@& Nat) → UInt8 → ByteArray
   | ⟨bs⟩, i, b => ⟨bs.set! i b⟩
@@ -199,18 +195,6 @@ instance : ToString ByteArray := ⟨fun bs => bs.toList.toString⟩
 
 /-- Interpret a `ByteArray` of size 8 as a little-endian `UInt64`. -/
 def ByteArray.toUInt64LE! (bs : ByteArray) : UInt64 :=
-  assert! bs.size == 8
-  (bs.get! 7).toUInt64 <<< 0x38 |||
-  (bs.get! 6).toUInt64 <<< 0x30 |||
-  (bs.get! 5).toUInt64 <<< 0x28 |||
-  (bs.get! 4).toUInt64 <<< 0x20 |||
-  (bs.get! 3).toUInt64 <<< 0x18 |||
-  (bs.get! 2).toUInt64 <<< 0x10 |||
-  (bs.get! 1).toUInt64 <<< 0x8  |||
-  (bs.get! 0).toUInt64
-
-/-- Interpret a `ByteArray` of size 8 as a big-endian `UInt64`. -/
-def ByteArray.toUInt64BE! (bs : ByteArray) : UInt64 :=
   assert! bs.size == 8
   (bs.get! 0).toUInt64 <<< 0x38 |||
   (bs.get! 1).toUInt64 <<< 0x30 |||
@@ -220,3 +204,15 @@ def ByteArray.toUInt64BE! (bs : ByteArray) : UInt64 :=
   (bs.get! 5).toUInt64 <<< 0x10 |||
   (bs.get! 6).toUInt64 <<< 0x8  |||
   (bs.get! 7).toUInt64
+
+/-- Interpret a `ByteArray` of size 8 as a big-endian `UInt64`. -/
+def ByteArray.toUInt64BE! (bs : ByteArray) : UInt64 :=
+  assert! bs.size == 8
+  (bs.get! 7).toUInt64 <<< 0x38 |||
+  (bs.get! 6).toUInt64 <<< 0x30 |||
+  (bs.get! 5).toUInt64 <<< 0x28 |||
+  (bs.get! 4).toUInt64 <<< 0x20 |||
+  (bs.get! 3).toUInt64 <<< 0x18 |||
+  (bs.get! 2).toUInt64 <<< 0x10 |||
+  (bs.get! 1).toUInt64 <<< 0x8  |||
+  (bs.get! 0).toUInt64

src/Init/Data/Channel.lean

@@ -41,7 +41,7 @@ Sends a message on an `Channel`.
 
 This function does not block.
 -/
-def Channel.send (ch : Channel α) (v : α) : BaseIO Unit :=
+def Channel.send (v : α) (ch : Channel α) : BaseIO Unit :=
   ch.atomically do
     let st ← get
     if st.closed then return

src/Init/Data/Fin/Basic.lean

@@ -4,7 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura, Robert Y. Lewis, Keeley Hoek, Mario Carneiro
 -/
 prelude
+import Init.Data.Nat.Div
 import Init.Data.Nat.Bitwise.Basic
+import Init.Coe
 
 open Nat
 
@@ -168,3 +170,9 @@ theorem val_add_one_le_of_lt {n : Nat} {a b : Fin n} (h : a < b) : (a : Nat) + 1
 theorem val_add_one_le_of_gt {n : Nat} {a b : Fin n} (h : a > b) : (b : Nat) + 1 ≤ (a : Nat) := h
 
 end Fin
+
+instance [GetElem cont Nat elem dom] : GetElem cont (Fin n) elem fun xs i => dom xs i where
+  getElem xs i h := getElem xs i.1 h
+
+macro_rules
+  | `(tactic| get_elem_tactic_trivial) => `(tactic| apply Fin.val_lt_of_le; get_elem_tactic_trivial; done)

src/Init/Data/Fin/Lemmas.lean

@@ -541,7 +541,7 @@ theorem pred_mk {n : Nat} (i : Nat) (h : i < n + 1) (w) : Fin.pred ⟨i, h⟩ w
     ∀ {a b : Fin (n + 1)} {ha : a ≠ 0} {hb : b ≠ 0}, a.pred ha = b.pred hb ↔ a = b
   | ⟨0, _⟩, _, ha, _ => by simp only [mk_zero, ne_eq, not_true] at ha
   | ⟨i + 1, _⟩, ⟨0, _⟩, _, hb => by simp only [mk_zero, ne_eq, not_true] at hb
-  | ⟨i + 1, hi⟩, ⟨j + 1, hj⟩, ha, hb => by simp [ext_iff, Nat.succ.injEq]
+  | ⟨i + 1, hi⟩, ⟨j + 1, hj⟩, ha, hb => by simp [ext_iff]
 
 @[simp] theorem pred_one {n : Nat} :
     Fin.pred (1 : Fin (n + 2)) (Ne.symm (Fin.ne_of_lt one_pos)) = 0 := rfl
@@ -683,7 +683,6 @@ and `cast` defines the inductive step using `motive i.succ`, inducting downwards
 termination_by n + 1 - i
 decreasing_by decreasing_with
   -- FIXME: we put the proof down here to avoid getting a dummy `have` in the definition
-  try simp only [Nat.succ_sub_succ_eq_sub]
   exact Nat.add_sub_add_right .. ▸ Nat.sub_lt_sub_left i.2 (Nat.lt_succ_self i)
 
 @[simp] theorem reverseInduction_last {n : Nat} {motive : Fin (n + 1) → Sort _} {zero succ} :

src/Init/Data/FloatArray/Basic.lean

@@ -58,13 +58,9 @@ def get? (ds : FloatArray) (i : Nat) : Option Float :=
 instance : GetElem FloatArray Nat Float fun xs i => i < xs.size where
   getElem xs i h := xs.get ⟨i, h⟩
 
-instance : LawfulGetElem FloatArray Nat Float fun xs i => i < xs.size where
-
 instance : GetElem FloatArray USize Float fun xs i => i.val < xs.size where
   getElem xs i h := xs.uget i h
 
-instance : LawfulGetElem FloatArray USize Float fun xs i => i.val < xs.size where
-
 @[extern "lean_float_array_uset"]
 def uset : (a : FloatArray) → (i : USize) → Float → i.toNat < a.size → FloatArray
   | ⟨ds⟩, i, v, h => ⟨ds.uset i v h⟩

src/Init/Data/Int/DivModLemmas.lean

@@ -8,7 +8,6 @@ prelude
 import Init.Data.Int.DivMod
 import Init.Data.Int.Order
 import Init.Data.Nat.Dvd
-import Init.RCases
 
 /-!
 # Lemmas about integer division needed to bootstrap `omega`.

src/Init/Data/Int/Lemmas.lean

@@ -6,7 +6,7 @@ Authors: Jeremy Avigad, Deniz Aydin, Floris van Doorn, Mario Carneiro
 prelude
 import Init.Data.Int.Basic
 import Init.Conv
-import Init.NotationExtra
+import Init.PropLemmas
 
 namespace Int
 

src/Init/Data/Int/Order.lean

@@ -6,6 +6,7 @@ Authors: Jeremy Avigad, Deniz Aydin, Floris van Doorn, Mario Carneiro
 prelude
 import Init.Data.Int.Lemmas
 import Init.ByCases
+import Init.RCases
 
 /-!
 # Results about the order properties of the integers, and the integers as an ordered ring.
@@ -998,8 +999,7 @@ theorem natAbs_add_le (a b : Int) : natAbs (a + b) ≤ natAbs a + natAbs b := by
   refine fun a b => subNatNat_elim a b.succ
     (fun m n i => n = b.succ → natAbs i ≤ (m + b).succ) ?_
     (fun i n (e : (n + i).succ = _) => ?_) rfl
-  · intro i n h
-    subst h
+  · rintro i n rfl
     rw [Nat.add_comm _ i, Nat.add_assoc]
     exact Nat.le_add_right i (b.succ + b).succ
   · apply succ_le_succ

src/Init/Data/List.lean

@@ -8,4 +8,3 @@ import Init.Data.List.Basic
 import Init.Data.List.BasicAux
 import Init.Data.List.Control
 import Init.Data.List.Lemmas
-import Init.Data.List.Impl

src/Init/Data/List/Basic.lean

@@ -7,7 +7,6 @@ prelude
 import Init.SimpLemmas
 import Init.Data.Nat.Basic
 import Init.Data.Nat.Div
-
 set_option linter.missingDocs true -- keep it documented
 open Decidable List
 
@@ -55,6 +54,15 @@ variable {α : Type u} {β : Type v} {γ : Type w}
 
 namespace List
 
+instance : GetElem (List α) Nat α fun as i => i < as.length where
+  getElem as i h := as.get ⟨i, h⟩
+
+@[simp] theorem cons_getElem_zero (a : α) (as : List α) (h : 0 < (a :: as).length) : getElem (a :: as) 0 h = a := by
+  rfl
+
+@[simp] theorem cons_getElem_succ (a : α) (as : List α) (i : Nat) (h : i + 1 < (a :: as).length) : getElem (a :: as) (i+1) h = getElem as i (Nat.lt_of_succ_lt_succ h) := by
+  rfl
+
 theorem length_add_eq_lengthTRAux (as : List α) (n : Nat) : as.length + n = as.lengthTRAux n := by
   induction as generalizing n with
   | nil  => simp [length, lengthTRAux]
@@ -450,7 +458,7 @@ contains the longest initial segment for which `p` returns true
 and the second part is everything else.
 
 * `span (· > 5) [6, 8, 9, 5, 2, 9] = ([6, 8, 9], [5, 2, 9])`
-* `span (· > 10) [6, 8, 9, 5, 2, 9] = ([], [6, 8, 9, 5, 2, 9])`
+* `span (· > 10) [6, 8, 9, 5, 2, 9] = ([6, 8, 9, 5, 2, 9], [])`
 -/
 @[inline] def span (p : α → Bool) (as : List α) : List α × List α :=
   loop as []
@@ -512,6 +520,11 @@ def drop : Nat → List α → List α
 @[simp] theorem drop_nil : ([] : List α).drop i = [] := by
   cases i <;> rfl
 
+theorem get_drop_eq_drop (as : List α) (i : Nat) (h : i < as.length) : as[i] :: as.drop (i+1) = as.drop i :=
+  match as, i with
+  | _::_, 0   => rfl
+  | _::_, i+1 => get_drop_eq_drop _ i _
+
 /--
 `O(min n |xs|)`. Returns the first `n` elements of `xs`, or the whole list if `n` is too large.
 * `take 0 [a, b, c, d, e] = []`

src/Init/Data/List/Impl.lean

@@ -1,261 +0,0 @@
-/-
-Copyright (c) 2016 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-
-prelude
-import Init.Data.Array.Lemmas
-
-/-!
-## Tail recursive implementations for `List` definitions.
-
-Many of the proofs require theorems about `Array`,
-so these are in a separate file to minimize imports.
--/
-
-namespace List
-
-/-- Tail recursive version of `erase`. -/
-@[inline] def setTR (l : List α) (n : Nat) (a : α) : List α := go l n #[] where
-  /-- Auxiliary for `setTR`: `setTR.go l a xs n acc = acc.toList ++ set xs a`,
-  unless `n ≥ l.length` in which case it returns `l` -/
-  go : List α → Nat → Array α → List α
-  | [], _, _ => l
-  | _::xs, 0, acc => acc.toListAppend (a::xs)
-  | x::xs, n+1, acc => go xs n (acc.push x)
-
-@[csimp] theorem set_eq_setTR : @set = @setTR := by
-  funext α l n a; simp [setTR]
-  let rec go (acc) : ∀ xs n, l = acc.data ++ xs →
-    setTR.go l a xs n acc = acc.data ++ xs.set n a
-  | [], _ => fun h => by simp [setTR.go, set, h]
-  | x::xs, 0 => by simp [setTR.go, set]
-  | x::xs, n+1 => fun h => by simp [setTR.go, set]; rw [go _ xs]; {simp}; simp [h]
-  exact (go #[] _ _ rfl).symm
-
-/-- Tail recursive version of `erase`. -/
-@[inline] def eraseTR [BEq α] (l : List α) (a : α) : List α := go l #[] where
-  /-- Auxiliary for `eraseTR`: `eraseTR.go l a xs acc = acc.toList ++ erase xs a`,
-  unless `a` is not present in which case it returns `l` -/
-  go : List α → Array α → List α
-  | [], _ => l
-  | x::xs, acc => bif x == a then acc.toListAppend xs else go xs (acc.push x)
-
-@[csimp] theorem erase_eq_eraseTR : @List.erase = @eraseTR := by
-  funext α _ l a; simp [eraseTR]
-  suffices ∀ xs acc, l = acc.data ++ xs → eraseTR.go l a xs acc = acc.data ++ xs.erase a from
-    (this l #[] (by simp)).symm
-  intro xs; induction xs with intro acc h
-  | nil => simp [List.erase, eraseTR.go, h]
-  | cons x xs IH =>
-    simp [List.erase, eraseTR.go]
-    cases x == a <;> simp
-    · rw [IH]; simp; simp; exact h
-
-/-- Tail recursive version of `eraseIdx`. -/
-@[inline] def eraseIdxTR (l : List α) (n : Nat) : List α := go l n #[] where
-  /-- Auxiliary for `eraseIdxTR`: `eraseIdxTR.go l n xs acc = acc.toList ++ eraseIdx xs a`,
-  unless `a` is not present in which case it returns `l` -/
-  go : List α → Nat → Array α → List α
-  | [], _, _ => l
-  | _::as, 0, acc => acc.toListAppend as
-  | a::as, n+1, acc => go as n (acc.push a)
-
-@[csimp] theorem eraseIdx_eq_eraseIdxTR : @eraseIdx = @eraseIdxTR := by
-  funext α l n; simp [eraseIdxTR]
-  suffices ∀ xs acc, l = acc.data ++ xs → eraseIdxTR.go l xs n acc = acc.data ++ xs.eraseIdx n from
-    (this l #[] (by simp)).symm
-  intro xs; induction xs generalizing n with intro acc h
-  | nil => simp [eraseIdx, eraseIdxTR.go, h]
-  | cons x xs IH =>
-    match n with
-    | 0 => simp [eraseIdx, eraseIdxTR.go]
-    | n+1 =>
-      simp [eraseIdx, eraseIdxTR.go]
-      rw [IH]; simp; simp; exact h
-
-/-- Tail recursive version of `bind`. -/
-@[inline] def bindTR (as : List α) (f : α → List β) : List β := go as #[] where
-  /-- Auxiliary for `bind`: `bind.go f as = acc.toList ++ bind f as` -/
-  @[specialize] go : List α → Array β → List β
-  | [], acc => acc.toList
-  | x::xs, acc => go xs (acc ++ f x)
-
-@[csimp] theorem bind_eq_bindTR : @List.bind = @bindTR := by
-  funext α β as f
-  let rec go : ∀ as acc, bindTR.go f as acc = acc.data ++ as.bind f
-    | [], acc => by simp [bindTR.go, bind]
-    | x::xs, acc => by simp [bindTR.go, bind, go xs]
-  exact (go as #[]).symm
-
-/-- Tail recursive version of `join`. -/
-@[inline] def joinTR (l : List (List α)) : List α := bindTR l id
-
-@[csimp] theorem join_eq_joinTR : @join = @joinTR := by
-  funext α l; rw [← List.bind_id, List.bind_eq_bindTR]; rfl
-
-/-- Tail recursive version of `filterMap`. -/
-@[inline] def filterMapTR (f : α → Option β) (l : List α) : List β := go l #[] where
-  /-- Auxiliary for `filterMap`: `filterMap.go f l = acc.toList ++ filterMap f l` -/
-  @[specialize] go : List α → Array β → List β
-  | [], acc => acc.toList
-  | a::as, acc => match f a with
-    | none => go as acc
-    | some b => go as (acc.push b)
-
-@[csimp] theorem filterMap_eq_filterMapTR : @List.filterMap = @filterMapTR := by
-  funext α β f l
-  let rec go : ∀ as acc, filterMapTR.go f as acc = acc.data ++ as.filterMap f
-    | [], acc => by simp [filterMapTR.go, filterMap]
-    | a::as, acc => by simp [filterMapTR.go, filterMap, go as]; split <;> simp [*]
-  exact (go l #[]).symm
-
-/-- Tail recursive version of `replace`. -/
-@[inline] def replaceTR [BEq α] (l : List α) (b c : α) : List α := go l #[] where
-  /-- Auxiliary for `replace`: `replace.go l b c xs acc = acc.toList ++ replace xs b c`,
-  unless `b` is not found in `xs` in which case it returns `l`. -/
-  @[specialize] go : List α → Array α → List α
-  | [], _ => l
-  | a::as, acc => bif a == b then acc.toListAppend (c::as) else go as (acc.push a)
-
-@[csimp] theorem replace_eq_replaceTR : @List.replace = @replaceTR := by
-  funext α _ l b c; simp [replaceTR]
-  suffices ∀ xs acc, l = acc.data ++ xs →
-      replaceTR.go l b c xs acc = acc.data ++ xs.replace b c from
-    (this l #[] (by simp)).symm
-  intro xs; induction xs with intro acc
-  | nil => simp [replace, replaceTR.go]
-  | cons x xs IH =>
-    simp [replace, replaceTR.go]; split <;> simp [*]
-    · intro h; rw [IH]; simp; simp; exact h
-
-/-- Tail recursive version of `take`. -/
-@[inline] def takeTR (n : Nat) (l : List α) : List α := go l n #[] where
-  /-- Auxiliary for `take`: `take.go l xs n acc = acc.toList ++ take n xs`,
-  unless `n ≥ xs.length` in which case it returns `l`. -/
-  @[specialize] go : List α → Nat → Array α → List α
-  | [], _, _ => l
-  | _::_, 0, acc => acc.toList
-  | a::as, n+1, acc => go as n (acc.push a)
-
-@[csimp] theorem take_eq_takeTR : @take = @takeTR := by
-  funext α n l; simp [takeTR]
-  suffices ∀ xs acc, l = acc.data ++ xs → takeTR.go l xs n acc = acc.data ++ xs.take n from
-    (this l #[] (by simp)).symm
-  intro xs; induction xs generalizing n with intro acc
-  | nil => cases n <;> simp [take, takeTR.go]
-  | cons x xs IH =>
-    cases n with simp [take, takeTR.go]
-    | succ n => intro h; rw [IH]; simp; simp; exact h
-
-/-- Tail recursive version of `takeWhile`. -/
-@[inline] def takeWhileTR (p : α → Bool) (l : List α) : List α := go l #[] where
-  /-- Auxiliary for `takeWhile`: `takeWhile.go p l xs acc = acc.toList ++ takeWhile p xs`,
-  unless no element satisfying `p` is found in `xs` in which case it returns `l`. -/
-  @[specialize] go : List α → Array α → List α
-  | [], _ => l
-  | a::as, acc => bif p a then go as (acc.push a) else acc.toList
-
-@[csimp] theorem takeWhile_eq_takeWhileTR : @takeWhile = @takeWhileTR := by
-  funext α p l; simp [takeWhileTR]
-  suffices ∀ xs acc, l = acc.data ++ xs →
-      takeWhileTR.go p l xs acc = acc.data ++ xs.takeWhile p from
-    (this l #[] (by simp)).symm
-  intro xs; induction xs with intro acc
-  | nil => simp [takeWhile, takeWhileTR.go]
-  | cons x xs IH =>
-    simp [takeWhile, takeWhileTR.go]; split <;> simp [*]
-    · intro h; rw [IH]; simp; simp; exact h
-
-/-- Tail recursive version of `foldr`. -/
-@[specialize] def foldrTR (f : α → β → β) (init : β) (l : List α) : β := l.toArray.foldr f init
-
-@[csimp] theorem foldr_eq_foldrTR : @foldr = @foldrTR := by
-  funext α β f init l; simp [foldrTR, Array.foldr_eq_foldr_data, -Array.size_toArray]
-
-/-- Tail recursive version of `zipWith`. -/
-@[inline] def zipWithTR (f : α → β → γ) (as : List α) (bs : List β) : List γ := go as bs #[] where
-  /-- Auxiliary for `zipWith`: `zipWith.go f as bs acc = acc.toList ++ zipWith f as bs` -/
-  go : List α → List β → Array γ → List γ
-  | a::as, b::bs, acc => go as bs (acc.push (f a b))
-  | _, _, acc => acc.toList
-
-@[csimp] theorem zipWith_eq_zipWithTR : @zipWith = @zipWithTR := by
-  funext α β γ f as bs
-  let rec go : ∀ as bs acc, zipWithTR.go f as bs acc = acc.data ++ as.zipWith f bs
-    | [], _, acc | _::_, [], acc => by simp [zipWithTR.go, zipWith]
-    | a::as, b::bs, acc => by simp [zipWithTR.go, zipWith, go as bs]
-  exact (go as bs #[]).symm
-
-/-- Tail recursive version of `unzip`. -/
-def unzipTR (l : List (α × β)) : List α × List β :=
-  l.foldr (fun (a, b) (al, bl) => (a::al, b::bl)) ([], [])
-
-@[csimp] theorem unzip_eq_unzipTR : @unzip = @unzipTR := by
-  funext α β l; simp [unzipTR]; induction l <;> simp [*]
-
-/-- Tail recursive version of `enumFrom`. -/
-def enumFromTR (n : Nat) (l : List α) : List (Nat × α) :=
-  let arr := l.toArray
-  (arr.foldr (fun a (n, acc) => (n-1, (n-1, a) :: acc)) (n + arr.size, [])).2
-
-@[csimp] theorem enumFrom_eq_enumFromTR : @enumFrom = @enumFromTR := by
-  funext α n l; simp [enumFromTR, -Array.size_toArray]
-  let f := fun (a : α) (n, acc) => (n-1, (n-1, a) :: acc)
-  let rec go : ∀ l n, l.foldr f (n + l.length, []) = (n, enumFrom n l)
-    | [], n => rfl
-    | a::as, n => by
-      rw [← show _ + as.length = n + (a::as).length from Nat.succ_add .., foldr, go as]
-      simp [enumFrom, f]
-  rw [Array.foldr_eq_foldr_data]
-  simp [go]
-
-theorem replicateTR_loop_eq : ∀ n, replicateTR.loop a n acc = replicate n a ++ acc
-  | 0 => rfl
-  | n+1 => by rw [← replicateTR_loop_replicate_eq _ 1 n, replicate, replicate,
-    replicateTR.loop, replicateTR_loop_eq n, replicateTR_loop_eq n, append_assoc]; rfl
-
-/-- Tail recursive version of `dropLast`. -/
-@[inline] def dropLastTR (l : List α) : List α := l.toArray.pop.toList
-
-@[csimp] theorem dropLast_eq_dropLastTR : @dropLast = @dropLastTR := by
-  funext α l; simp [dropLastTR]
-
-/-- Tail recursive version of `intersperse`. -/
-def intersperseTR (sep : α) : List α → List α
-  | [] => []
-  | [x] => [x]
-  | x::y::xs => x :: sep :: y :: xs.foldr (fun a r => sep :: a :: r) []
-
-@[csimp] theorem intersperse_eq_intersperseTR : @intersperse = @intersperseTR := by
-  funext α sep l; simp [intersperseTR]
-  match l with
-  | [] | [_] => rfl
-  | x::y::xs => simp [intersperse]; induction xs generalizing y <;> simp [*]
-
-/-- Tail recursive version of `intercalate`. -/
-def intercalateTR (sep : List α) : List (List α) → List α
-  | [] => []
-  | [x] => x
-  | x::xs => go sep.toArray x xs #[]
-where
-  /-- Auxiliary for `intercalateTR`:
-  `intercalateTR.go sep x xs acc = acc.toList ++ intercalate sep.toList (x::xs)` -/
-  go (sep : Array α) : List α → List (List α) → Array α → List α
-  | x, [], acc => acc.toListAppend x
-  | x, y::xs, acc => go sep y xs (acc ++ x ++ sep)
-
-@[csimp] theorem intercalate_eq_intercalateTR : @intercalate = @intercalateTR := by
-  funext α sep l; simp [intercalate, intercalateTR]
-  match l with
-  | [] => rfl
-  | [_] => simp
-  | x::y::xs =>
-    let rec go {acc x} : ∀ xs,
-      intercalateTR.go sep.toArray x xs acc = acc.data ++ join (intersperse sep (x::xs))
-    | [] => by simp [intercalateTR.go]
-    | _::_ => by simp [intercalateTR.go, go]
-    simp [intersperse, go]
-
-end List

src/Init/Data/List/Lemmas.lean

@@ -249,14 +249,12 @@ theorem getD_eq_get? : ∀ l n (a : α), getD l n a = (get? l n).getD a
 theorem get?_append_right : ∀ {l₁ l₂ : List α} {n : Nat}, l₁.length ≤ n →
   (l₁ ++ l₂).get? n = l₂.get? (n - l₁.length)
 | [], _, n, _ => rfl
-| a :: l, _, n+1, h₁ => by
-  rw [cons_append]
-  simp [Nat.succ_sub_succ_eq_sub, get?_append_right (Nat.lt_succ.1 h₁)]
+| a :: l, _, n+1, h₁ => by rw [cons_append]; simp [get?_append_right (Nat.lt_succ.1 h₁)]
 
 theorem get?_reverse' : ∀ {l : List α} (i j), i + j + 1 = length l →
     get? l.reverse i = get? l j
   | [], _, _, _ => rfl
-  | a::l, i, 0, h => by simp [Nat.succ.injEq] at h; simp [h, get?_append_right, Nat.succ.injEq]
+  | a::l, i, 0, h => by simp at h; simp [h, get?_append_right]
   | a::l, i, j+1, h => by
     have := Nat.succ.inj h; simp at this ⊢
     rw [get?_append, get?_reverse' _ j this]
@@ -268,12 +266,6 @@ theorem get?_reverse {l : List α} (i) (h : i < length l) :
     rw [Nat.add_sub_of_le (Nat.le_sub_one_of_lt h),
       Nat.sub_add_cancel (Nat.lt_of_le_of_lt (Nat.zero_le _) h)]
 
-@[simp] theorem getD_nil : getD [] n d = d := rfl
-
-@[simp] theorem getD_cons_zero : getD (x :: xs) 0 d = x := rfl
-
-@[simp] theorem getD_cons_succ : getD (x :: xs) (n + 1) d = getD xs n d := rfl
-
 /-! ### take and drop -/
 
 @[simp] theorem take_append_drop : ∀ (n : Nat) (l : List α), take n l ++ drop n l = l
@@ -713,5 +705,3 @@ theorem minimum?_eq_some_iff [Min α] [LE α] [anti : Antisymm ((· : α) ≤ ·
   | _ :: l, i + 1, j + 1 => by
     have g : i ≠ j := h ∘ congrArg (· + 1)
     simp [get_set_ne l g]
-
-end List

src/Init/Data/Nat.lean

@@ -19,4 +19,3 @@ import Init.Data.Nat.Lemmas
 import Init.Data.Nat.Mod
 import Init.Data.Nat.Lcm
 import Init.Data.Nat.Compare
-import Init.Data.Nat.Simproc

src/Init/Data/Nat/Basic.lean

@@ -174,7 +174,7 @@ protected theorem add_right_comm (n m k : Nat) : (n + m) + k = (n + k) + m := by
 protected theorem add_left_cancel {n m k : Nat} : n + m = n + k → m = k := by
   induction n with
   | zero => simp
-  | succ n ih => simp [succ_add, succ.injEq]; intro h; apply ih h
+  | succ n ih => simp [succ_add]; intro h; apply ih h
 
 protected theorem add_right_cancel {n m k : Nat} (h : n + m = k + m) : n = k := by
   rw [Nat.add_comm n m, Nat.add_comm k m] at h
@@ -248,7 +248,7 @@ theorem lt_succ_of_le {n m : Nat} : n ≤ m → n < succ m := succ_le_succ
 
 @[simp] protected theorem sub_zero (n : Nat) : n - 0 = n := rfl
 
-theorem succ_sub_succ_eq_sub (n m : Nat) : succ n - succ m = n - m := by
+@[simp] theorem succ_sub_succ_eq_sub (n m : Nat) : succ n - succ m = n - m := by
   induction m with
   | zero      => exact rfl
   | succ m ih => apply congrArg pred ih
@@ -574,7 +574,7 @@ theorem eq_zero_or_eq_succ_pred : ∀ n, n = 0 ∨ n = succ (pred n)
   | 0 => .inl rfl
   | _+1 => .inr rfl
 
-theorem succ_inj' : succ a = succ b ↔ a = b := (Nat.succ.injEq a b).to_iff
+theorem succ_inj' : succ a = succ b ↔ a = b := ⟨succ.inj, congrArg _⟩
 
 theorem succ_le_succ_iff : succ a ≤ succ b ↔ a ≤ b := ⟨le_of_succ_le_succ, succ_le_succ⟩
 
@@ -802,7 +802,7 @@ theorem add_sub_of_le {a b : Nat} (h : a ≤ b) : a + (b - a) = b := by
 protected theorem add_sub_add_right (n k m : Nat) : (n + k) - (m + k) = n - m := by
   induction k with
   | zero => simp
-  | succ k ih => simp [← Nat.add_assoc, succ_sub_succ_eq_sub, ih]
+  | succ k ih => simp [← Nat.add_assoc, ih]
 
 protected theorem add_sub_add_left (k n m : Nat) : (k + n) - (k + m) = n - m := by
   rw [Nat.add_comm k n, Nat.add_comm k m, Nat.add_sub_add_right]

src/Init/Data/Nat/Bitwise/Lemmas.lean

@@ -9,7 +9,6 @@ import Init.Data.Bool
 import Init.Data.Int.Pow
 import Init.Data.Nat.Bitwise.Basic
 import Init.Data.Nat.Lemmas
-import Init.Data.Nat.Simproc
 import Init.TacticsExtra
 import Init.Omega
 
@@ -272,7 +271,7 @@ theorem testBit_two_pow_sub_succ (h₂ : x < 2 ^ n) (i : Nat) :
   induction i generalizing n x with
   | zero =>
     match n with
-    | 0 => simp [succ_sub_succ_eq_sub]
+    | 0 => simp
     | n+1 =>
       simp [not_decide_mod_two_eq_one]
       omega
@@ -280,7 +279,7 @@ theorem testBit_two_pow_sub_succ (h₂ : x < 2 ^ n) (i : Nat) :
     simp only [testBit_succ]
     match n with
     | 0 =>
-      simp [decide_eq_false, succ_sub_succ_eq_sub]
+      simp [decide_eq_false]
     | n+1 =>
       rw [Nat.two_pow_succ_sub_succ_div_two, ih]
       · simp [Nat.succ_lt_succ_iff]

src/Init/Data/Nat/Lemmas.lean

@@ -88,7 +88,7 @@ protected theorem add_pos_right (m) (h : 0 < n) : 0 < m + n :=
   Nat.lt_of_lt_of_le h (Nat.le_add_left ..)
 
 protected theorem add_self_ne_one : ∀ n, n + n ≠ 1
-  | n+1, h => by rw [Nat.succ_add, Nat.succ.injEq] at h; contradiction
+  | n+1, h => by rw [Nat.succ_add, Nat.succ_inj'] at h; contradiction
 
 /-! ## sub -/
 

src/Init/Data/Nat/Linear.lean

@@ -580,7 +580,7 @@ attribute [-simp] Nat.right_distrib Nat.left_distrib
 
 theorem PolyCnstr.denote_mul (ctx : Context) (k : Nat) (c : PolyCnstr) : (c.mul (k+1)).denote ctx = c.denote ctx := by
   cases c; rename_i eq lhs rhs
-  have : k ≠ 0 → k + 1 ≠ 1 := by intro h; match k with | 0 => contradiction | k+1 => simp [Nat.succ.injEq]
+  have : k ≠ 0 → k + 1 ≠ 1 := by intro h; match k with | 0 => contradiction | k+1 => simp
   have : ¬ (k == 0) → (k + 1 == 1) = false := fun h => beq_false_of_ne (this (ne_of_beq_false (Bool.of_not_eq_true h)))
   have : ¬ ((k + 1 == 0) = true)  := fun h => absurd (eq_of_beq h) (Nat.succ_ne_zero k)
   have : (1 == (0 : Nat)) = false := rfl

src/Init/Data/Nat/Simproc.lean

@@ -1,108 +0,0 @@
-/-
-Copyright (c) 2023 Lean FRO. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Joe Hendrix
--/
-prelude
-import Init.Data.Bool
-import Init.Data.Nat.Basic
-import Init.Data.Nat.Lemmas
-
-/-!
-This contains lemmas used by the Nat simprocs for simplifying arithmetic
-addition offsets.
--/
-namespace Nat.Simproc
-
-/- Sub proofs -/
-
-theorem sub_add_eq_comm (a b c : Nat) : a - (b + c) = a - c - b := by
-  rw [Nat.add_comm b c]
-  exact Nat.sub_add_eq a c b
-
-theorem add_sub_add_le (a c : Nat) {b d : Nat} (h : b ≤ d) : a + b - (c + d) = a - (c + (d-b)) := by
-  induction b generalizing a c d with
-  | zero =>
-    simp
-  | succ b ind =>
-    match d with
-    | 0 =>
-      contradiction
-    | d + 1 =>
-      have g := Nat.le_of_succ_le_succ h
-      rw [Nat.add_succ a, Nat.add_succ c, Nat.succ_sub_succ, Nat.succ_sub_succ,
-          ind _ _ g]
-
-theorem add_sub_add_ge (a c : Nat) {b d : Nat} (h : b ≥ d) : a + b - (c + d) = a + (b - d) - c := by
-  rw [Nat.add_comm c d, Nat.sub_add_eq, Nat.add_sub_assoc h a]
-
-theorem add_sub_le (a : Nat) {b c : Nat} (h : b ≤ c) : a + b - c = a - (c - b) := by
-  have p := add_sub_add_le a 0 h
-  simp only [Nat.zero_add] at p
-  exact p
-
-/- Eq proofs -/
-
-theorem add_eq_gt (a : Nat) {b c : Nat} (h : b > c) : (a + b = c) = False :=
-  eq_false (Nat.ne_of_gt (Nat.lt_of_lt_of_le h (le_add_left b a)))
-
-theorem eq_add_gt (a : Nat) {b c : Nat} (h : c > a) : (a = b + c) = False := by
-  rw [@Eq.comm Nat a (b + c)]
-  exact add_eq_gt b h
-
-theorem add_eq_add_le (a c : Nat) {b d : Nat} (h : b ≤ d) : (a + b = c + d) = (a = c + (d - b)) := by
-  have g : b ≤ c + d := Nat.le_trans h (le_add_left d c)
-  rw [← Nat.add_sub_assoc h, @Eq.comm _ a, Nat.sub_eq_iff_eq_add g, @Eq.comm _ (a + b)]
-
-theorem add_eq_add_ge (a c : Nat) {b d : Nat} (h : b ≥ d) : (a + b = c + d) = (a + (b - d) = c) := by
-  rw [@Eq.comm _ (a + b) _, add_eq_add_le c a h, @Eq.comm _ _ c]
-
-theorem add_eq_le (a : Nat) {b c : Nat} (h : b ≤ c) : (a + b = c) = (a = c - b) := by
-  have r := add_eq_add_le a 0 h
-  simp only [Nat.zero_add] at r
-  exact r
-
-theorem eq_add_le {a : Nat} (b : Nat) {c : Nat} (h : c ≤ a) : (a = b + c) = (b = a - c) := by
-  rw [@Eq.comm Nat a (b + c)]
-  exact add_eq_le b h
-
-/- Lemmas for lifting Eq proofs to beq -/
-
-theorem beqEqOfEqEq {a b c d : Nat} (p : (a = b) = (c = d)) : (a == b) = (c == d) := by
-  simp only [Bool.beq_eq_decide_eq, p]
-
-theorem beqFalseOfEqFalse {a b : Nat} (p : (a = b) = False) : (a == b) = false := by
-  simp [Bool.beq_eq_decide_eq, p]
-
-theorem bneEqOfEqEq {a b c d : Nat} (p : (a = b) = (c = d)) : (a != b) = (c != d) := by
-  simp only [bne, beqEqOfEqEq p]
-
-theorem bneTrueOfEqFalse {a b : Nat} (p : (a = b) = False) : (a != b) = true := by
-  simp [bne, beqFalseOfEqFalse p]
-
-/- le proofs -/
-
-theorem add_le_add_le (a c : Nat) {b d : Nat} (h : b ≤ d) : (a + b ≤ c + d) = (a ≤ c + (d - b)) := by
-  rw [← Nat.add_sub_assoc h, Nat.le_sub_iff_add_le]
-  exact Nat.le_trans h (le_add_left d c)
-
-theorem add_le_add_ge (a c : Nat) {b d : Nat} (h : b ≥ d) : (a + b ≤ c + d) = (a + (b - d) ≤ c) := by
-  rw [← Nat.add_sub_assoc h, Nat.sub_le_iff_le_add]
-
-theorem add_le_le (a : Nat) {b c : Nat} (h : b ≤ c) : (a + b ≤ c) = (a ≤ c - b) := by
-  have r := add_le_add_le a 0 h
-  simp only [Nat.zero_add] at r
-  exact r
-
-theorem add_le_gt (a : Nat) {b c : Nat} (h : b > c) : (a + b ≤ c) = False :=
-  eq_false (Nat.not_le_of_gt (Nat.lt_of_lt_of_le h (le_add_left b a)))
-
-theorem le_add_le (a : Nat) {b c : Nat} (h : a ≤ c) : (a ≤ b + c) = True :=
-  eq_true (Nat.le_trans h (le_add_left c b))
-
-theorem le_add_ge (a : Nat) {b c : Nat} (h : a ≥ c) : (a ≤ b + c) = (a - c ≤ b) := by
-  have r := add_le_add_ge 0 b h
-  simp only [Nat.zero_add] at r
-  exact r
-
-end Nat.Simproc

src/Init/Data/Option/Basic.lean

@@ -37,13 +37,6 @@ def toMonad [Monad m] [Alternative m] : Option α → m α
   | none,   _ => none
   | some a, b => b a
 
-/-- Runs `f` on `o`'s value, if any, and returns its result, or else returns `none`.  -/
-@[inline] protected def bindM [Monad m] (f : α → m (Option β)) (o : Option α) : m (Option β) := do
-  if let some a := o then
-    return (← f a)
-  else
-    return none
-
 @[inline] protected def mapM [Monad m] (f : α → m β) (o : Option α) : m (Option β) := do
   if let some a := o then
     return some (← f a)

src/Init/Data/Ord.lean

@@ -6,7 +6,6 @@ Authors: Dany Fabian, Sebastian Ullrich
 
 prelude
 import Init.Data.String
-import Init.Data.Array.Basic
 
 inductive Ordering where
   | lt | eq | gt
@@ -88,24 +87,11 @@ def isGE : Ordering → Bool
 
 end Ordering
 
-/--
-Yields an `Ordering` s.t. `x < y` corresponds to `Ordering.lt` / `Ordering.gt` and
-`x = y` corresponds to `Ordering.eq`.
--/
 @[inline] def compareOfLessAndEq {α} (x y : α) [LT α] [Decidable (x < y)] [DecidableEq α] : Ordering :=
   if x < y then Ordering.lt
   else if x = y then Ordering.eq
   else Ordering.gt
 
-/--
-Yields an `Ordering` s.t. `x < y` corresponds to `Ordering.lt` / `Ordering.gt` and
-`x == y` corresponds to `Ordering.eq`.
--/
-@[inline] def compareOfLessAndBEq {α} (x y : α) [LT α] [Decidable (x < y)] [BEq α] : Ordering :=
-  if x < y then .lt
-  else if x == y then .eq
-  else .gt
-
 /--
 Compare `a` and `b` lexicographically by `cmp₁` and `cmp₂`. `a` and `b` are
 first compared by `cmp₁`. If this returns 'equal', `a` and `b` are compared
@@ -119,7 +105,6 @@ class Ord (α : Type u) where
 
 export Ord (compare)
 
-set_option linter.unusedVariables false in  -- allow specifying `ord` explicitly
 /--
 Compare `x` and `y` by comparing `f x` and `f y`.
 -/
@@ -162,13 +147,6 @@ instance : Ord USize where
 instance : Ord Char where
   compare x y := compareOfLessAndEq x y
 
-instance [Ord α] : Ord (Option α) where
-  compare
-  | none,   none   => .eq
-  | none,   some _ => .lt
-  | some _, none   => .gt
-  | some x, some y => compare x y
-
 /-- The lexicographic order on pairs. -/
 def lexOrd [Ord α] [Ord β] : Ord (α × β) where
   compare p1 p2 := match compare p1.1 p2.1 with
@@ -216,7 +194,7 @@ protected def opposite (ord : Ord α) : Ord α where
 /--
 `ord.on f` compares `x` and `y` by comparing `f x` and `f y` according to `ord`.
 -/
-protected def on (_ : Ord β) (f : α → β) : Ord α where
+protected def on (ord : Ord β) (f : α → β) : Ord α where
   compare := compareOn f
 
 /--
@@ -232,13 +210,4 @@ returns 'equal', by `ord₂`.
 protected def lex' (ord₁ ord₂ : Ord α) : Ord α where
   compare := compareLex ord₁.compare ord₂.compare
 
-/--
-Creates an order which compares elements of an `Array` in lexicographic order.
--/
-protected def arrayOrd [a : Ord α] : Ord (Array α) where
-  compare x y :=
-    let _ : LT α := a.toLT
-    let _ : BEq α := a.toBEq
-    compareOfLessAndBEq x.toList y.toList
-
 end Ord

src/Init/Data/String/Basic.lean

@@ -245,21 +245,12 @@ termination_by s.endPos.1 - i.1
 @[specialize] def split (s : String) (p : Char → Bool) : List String :=
   splitAux s p 0 0 []
 
-/--
-Auxiliary for `splitOn`. Preconditions:
-* `sep` is not empty
-* `b <= i` are indexes into `s`
-* `j` is an index into `sep`, and not at the end
-
-It represents the state where we have currently parsed some split parts into `r` (in reverse order),
-`b` is the beginning of the string / the end of the previous match of `sep`, and the first `j` bytes
-of `sep` match the bytes `i-j .. i` of `s`.
--/
 def splitOnAux (s sep : String) (b : Pos) (i : Pos) (j : Pos) (r : List String) : List String :=
-  if s.atEnd i then
+  if h : s.atEnd i then
     let r := (s.extract b i)::r
     r.reverse
   else
+    have := Nat.sub_lt_sub_left (Nat.gt_of_not_le (mt decide_eq_true h)) (lt_next s _)
     if s.get i == sep.get j then
       let i := s.next i
       let j := sep.next j
@@ -268,42 +259,9 @@ def splitOnAux (s sep : String) (b : Pos) (i : Pos) (j : Pos) (r : List String)
       else
         splitOnAux s sep b i j r
     else
-      splitOnAux s sep b (s.next (i - j)) 0 r
-termination_by (s.endPos.1 - (i - j).1, sep.endPos.1 - j.1)
-decreasing_by
-  all_goals simp_wf
-  focus
-    rename_i h _ _
-    left; exact Nat.sub_lt_sub_left
-      (Nat.lt_of_le_of_lt (Nat.sub_le ..) (Nat.gt_of_not_le (mt decide_eq_true h)))
-      (Nat.lt_of_le_of_lt (Nat.sub_le ..) (lt_next s _))
-  focus
-    rename_i i₀ j₀ _ eq h'
-    rw [show (s.next i₀ - sep.next j₀).1 = (i₀ - j₀).1 by
-      show (_ + csize _) - (_ + csize _) = _
-      rw [(beq_iff_eq ..).1 eq, Nat.add_sub_add_right]; rfl]
-    right; exact Nat.sub_lt_sub_left
-      (Nat.lt_of_le_of_lt (Nat.le_add_right ..) (Nat.gt_of_not_le (mt decide_eq_true h')))
-      (lt_next sep _)
-  focus
-    rename_i h _
-    left; exact Nat.sub_lt_sub_left
-      (Nat.lt_of_le_of_lt (Nat.sub_le ..) (Nat.gt_of_not_le (mt decide_eq_true h)))
-      (lt_next s _)
+      splitOnAux s sep b (s.next i) 0 r
+termination_by s.endPos.1 - i.1
 
-/--
-Splits a string `s` on occurrences of the separator `sep`. When `sep` is empty, it returns `[s]`;
-when `sep` occurs in overlapping patterns, the first match is taken. There will always be exactly
-`n+1` elements in the returned list if there were `n` nonoverlapping matches of `sep` in the string.
-The default separator is `" "`. The separators are not included in the returned substrings.
-
-```
-"here is some text ".splitOn = ["here", "is", "some", "text", ""]
-"here is some text ".splitOn "some" = ["here is ", " text "]
-"here is some text ".splitOn "" = ["here is some text "]
-"ababacabac".splitOn "aba" = ["", "bac", "c"]
-```
--/
 def splitOn (s : String) (sep : String := " ") : List String :=
   if sep == "" then [s] else splitOnAux s sep 0 0 0 []
 

src/Init/Data/String/Extra.lean

@@ -62,40 +62,4 @@ namespace Iterator
 
 end Iterator
 
-private def findLeadingSpacesSize (s : String) : Nat :=
-  let it := s.iter
-  let it := it.find (· == '\n') |>.next
-  consumeSpaces it 0 s.length
-where
-  consumeSpaces (it : String.Iterator) (curr min : Nat) : Nat :=
-    if it.atEnd then min
-    else if it.curr == ' ' || it.curr == '\t' then consumeSpaces it.next (curr + 1) min
-    else if it.curr == '\n' then findNextLine it.next min
-    else findNextLine it.next (Nat.min curr min)
-  findNextLine (it : String.Iterator) (min : Nat) : Nat :=
-    if it.atEnd then min
-    else if it.curr == '\n' then consumeSpaces it.next 0 min
-    else findNextLine it.next min
-
-private def removeNumLeadingSpaces (n : Nat) (s : String) : String :=
-  consumeSpaces n s.iter ""
-where
-  consumeSpaces (n : Nat) (it : String.Iterator) (r : String) : String :=
-     match n with
-     | 0 => saveLine it r
-     | n+1 =>
-       if it.atEnd then r
-       else if it.curr == ' ' || it.curr == '\t' then consumeSpaces n it.next r
-       else saveLine it r
-  termination_by (it, 1)
-  saveLine (it : String.Iterator) (r : String) : String :=
-    if it.atEnd then r
-    else if it.curr == '\n' then consumeSpaces n it.next (r.push '\n')
-    else saveLine it.next (r.push it.curr)
-  termination_by (it, 0)
-
-def removeLeadingSpaces (s : String) : String :=
-  let n := findLeadingSpacesSize s
-  if n == 0 then s else removeNumLeadingSpaces n s
-
 end String

src/Init/Ext.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner, Mario Carneiro
 -/
 prelude
-import Init.Data.ToString.Macro
 import Init.TacticsExtra
 import Init.RCases
 

src/Init/GetElem.lean

@@ -1,173 +0,0 @@
-/-
-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
--/
-prelude
-import Init.Util
-
-@[never_extract]
-private def outOfBounds [Inhabited α] : α :=
-  panic! "index out of bounds"
-
-/--
-The class `GetElem coll idx elem valid` implements the `xs[i]` notation.
-Given `xs[i]` with `xs : coll` and `i : idx`, Lean looks for an instance of
-`GetElem coll idx elem valid` and uses this to infer the type of return
-value `elem` and side conditions `valid` required to ensure `xs[i]` yields
-a valid value of type `elem`.
-
-For example, the instance for arrays looks like
-`GetElem (Array α) Nat α (fun xs i => i < xs.size)`.
-
-The proof side-condition `valid xs i` is automatically dispatched by the
-`get_elem_tactic` tactic, which can be extended by adding more clauses to
-`get_elem_tactic_trivial`.
--/
-class GetElem (coll : Type u) (idx : Type v) (elem : outParam (Type w))
-              (valid : outParam (coll → idx → Prop)) where
-  /--
-  The syntax `arr[i]` gets the `i`'th element of the collection `arr`. If there
-  are proof side conditions to the application, they will be automatically
-  inferred by the `get_elem_tactic` tactic.
-
-  The actual behavior of this class is type-dependent, but here are some
-  important implementations:
-  * `arr[i] : α` where `arr : Array α` and `i : Nat` or `i : USize`: does array
-    indexing with no bounds check and a proof side goal `i < arr.size`.
-  * `l[i] : α` where `l : List α` and `i : Nat`: index into a list, with proof
-    side goal `i < l.length`.
-  * `stx[i] : Syntax` where `stx : Syntax` and `i : Nat`: get a syntax argument,
-    no side goal (returns `.missing` out of range)
-
-  There are other variations on this syntax:
-  * `arr[i]!` is syntax for `getElem! arr i` which should panic and return
-    `default : α` if the index is not valid.
-  * `arr[i]?` is syntax for `getElem?` which should return `none` if the index
-    is not valid.
-  * `arr[i]'h` is syntax for `getElem arr i h` with `h` an explicit proof the
-    index is valid.
-  -/
-  getElem (xs : coll) (i : idx) (h : valid xs i) : elem
-
-  getElem? (xs : coll) (i : idx) [Decidable (valid xs i)] : Option elem :=
-    if h : _ then some (getElem xs i h) else none
-
-  getElem! [Inhabited elem] (xs : coll) (i : idx) [Decidable (valid xs i)] : elem :=
-    match getElem? xs i with | some e => e | none => outOfBounds
-
-export GetElem (getElem getElem! getElem?)
-
-@[inherit_doc getElem]
-syntax:max term noWs "[" withoutPosition(term) "]" : term
-macro_rules | `($x[$i]) => `(getElem $x $i (by get_elem_tactic))
-
-@[inherit_doc getElem]
-syntax term noWs "[" withoutPosition(term) "]'" term:max : term
-macro_rules | `($x[$i]'$h) => `(getElem $x $i $h)
-
-/--
-The syntax `arr[i]?` gets the `i`'th element of the collection `arr` or
-returns `none` if `i` is out of bounds.
--/
-macro:max x:term noWs "[" i:term "]" noWs "?" : term => `(getElem? $x $i)
-
-/--
-The syntax `arr[i]!` gets the `i`'th element of the collection `arr` and
-panics `i` is out of bounds.
--/
-macro:max x:term noWs "[" i:term "]" noWs "!" : term => `(getElem! $x $i)
-
-class LawfulGetElem (cont : Type u) (idx : Type v) (elem : outParam (Type w))
-   (dom : outParam (cont → idx → Prop)) [ge : GetElem cont idx elem dom] : Prop where
-
-  getElem?_def (c : cont) (i : idx) [Decidable (dom c i)] :
-    c[i]? = if h : dom c i then some (c[i]'h) else none := by intros; eq_refl
-  getElem!_def [Inhabited elem] (c : cont) (i : idx) [Decidable (dom c i)] :
-    c[i]! = match c[i]? with | some e => e | none => default := by intros; eq_refl
-
-export LawfulGetElem (getElem?_def getElem!_def)
-
-theorem getElem?_pos [GetElem cont idx elem dom] [LawfulGetElem cont idx elem dom]
-    (c : cont) (i : idx) (h : dom c i) [Decidable (dom c i)] : c[i]? = some (c[i]'h) := by
-  rw [getElem?_def]
-  exact dif_pos h
-
-theorem getElem?_neg [GetElem cont idx elem dom] [LawfulGetElem cont idx elem dom]
-    (c : cont) (i : idx) (h : ¬dom c i) [Decidable (dom c i)] : c[i]? = none := by
-  rw [getElem?_def]
-  exact dif_neg h
-
-theorem getElem!_pos [GetElem cont idx elem dom] [LawfulGetElem cont idx elem dom]
-    [Inhabited elem] (c : cont) (i : idx) (h : dom c i) [Decidable (dom c i)] :
-    c[i]! = c[i]'h := by
-  simp only [getElem!_def, getElem?_def, h]
-
-theorem getElem!_neg [GetElem cont idx elem dom] [LawfulGetElem cont idx elem dom]
-    [Inhabited elem] (c : cont) (i : idx) (h : ¬dom c i) [Decidable (dom c i)] : c[i]! = default := by
-  simp only [getElem!_def, getElem?_def, h]
-
-namespace Fin
-
-instance instGetElemFinVal [GetElem cont Nat elem dom] : GetElem cont (Fin n) elem fun xs i => dom xs i where
-  getElem xs i h := getElem xs i.1 h
-  getElem? xs i := getElem? xs i.val
-  getElem! xs i := getElem! xs i.val
-
-instance [GetElem cont Nat elem dom] [h : LawfulGetElem cont Nat elem dom] :
-      LawfulGetElem cont (Fin n) elem fun xs i => dom xs i where
-
-  getElem?_def _c _i _d := h.getElem?_def ..
-  getElem!_def _c _i _d := h.getElem!_def ..
-
-@[simp] theorem getElem_fin [GetElem Cont Nat Elem Dom] (a : Cont) (i : Fin n) (h : Dom a i) :
-    a[i] = a[i.1] := rfl
-
-@[simp] theorem getElem?_fin [h : GetElem Cont Nat Elem Dom] (a : Cont) (i : Fin n)
-    [Decidable (Dom a i)] : a[i]? = a[i.1]? := by rfl
-
-@[simp] theorem getElem!_fin [GetElem Cont Nat Elem Dom] (a : Cont) (i : Fin n)
-    [Decidable (Dom a i)] [Inhabited Elem] : a[i]! = a[i.1]! := rfl
-
-macro_rules
-  | `(tactic| get_elem_tactic_trivial) => `(tactic| apply Fin.val_lt_of_le; get_elem_tactic_trivial; done)
-
-end Fin
-
-namespace List
-
-instance : GetElem (List α) Nat α fun as i => i < as.length where
-  getElem as i h := as.get ⟨i, h⟩
-
-instance : LawfulGetElem (List α) Nat α fun as i => i < as.length where
-
-@[simp] theorem cons_getElem_zero (a : α) (as : List α) (h : 0 < (a :: as).length) : getElem (a :: as) 0 h = a := by
-  rfl
-
-@[simp] theorem cons_getElem_succ (a : α) (as : List α) (i : Nat) (h : i + 1 < (a :: as).length) : getElem (a :: as) (i+1) h = getElem as i (Nat.lt_of_succ_lt_succ h) := by
-  rfl
-
-theorem get_drop_eq_drop (as : List α) (i : Nat) (h : i < as.length) : as[i] :: as.drop (i+1) = as.drop i :=
-  match as, i with
-  | _::_, 0   => rfl
-  | _::_, i+1 => get_drop_eq_drop _ i _
-
-end List
-
-namespace Array
-
-instance : GetElem (Array α) Nat α fun xs i => i < xs.size where
-  getElem xs i h := xs.get ⟨i, h⟩
-
-instance : LawfulGetElem (Array α) Nat α fun xs i => i < xs.size where
-
-end Array
-
-namespace Lean.Syntax
-
-instance : GetElem Syntax Nat Syntax fun _ _ => True where
-  getElem stx i _ := stx.getArg i
-
-instance : LawfulGetElem Syntax Nat Syntax fun _ _ => True where
-
-end Lean.Syntax

src/Init/MacroTrace.lean

@@ -1,18 +0,0 @@
-/-
-Copyright (c) 2020 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
-
-Extra notation that depends on Init/Meta
--/
-
-prelude
-import Init.Data.ToString.Macro
-import Init.Meta
-
-namespace Lean
-
-macro "Macro.trace[" id:ident "]" s:interpolatedStr(term) : term =>
-  `(Macro.trace $(quote id.getId.eraseMacroScopes) (s! $s))
-
-end Lean

src/Init/Meta.lean

@@ -9,6 +9,7 @@ prelude
 import Init.MetaTypes
 import Init.Data.Array.Basic
 import Init.Data.Option.BasicAux
+import Init.Data.String.Extra
 
 namespace Lean
 
@@ -104,6 +105,43 @@ def idBeginEscape := '«'
 def idEndEscape   := '»'
 def isIdBeginEscape (c : Char) : Bool := c = idBeginEscape
 def isIdEndEscape (c : Char) : Bool := c = idEndEscape
+
+private def findLeadingSpacesSize (s : String) : Nat :=
+  let it := s.iter
+  let it := it.find (· == '\n') |>.next
+  consumeSpaces it 0 s.length
+where
+  consumeSpaces (it : String.Iterator) (curr min : Nat) : Nat :=
+    if it.atEnd then min
+    else if it.curr == ' ' || it.curr == '\t' then consumeSpaces it.next (curr + 1) min
+    else if it.curr == '\n' then findNextLine it.next min
+    else findNextLine it.next (Nat.min curr min)
+  findNextLine (it : String.Iterator) (min : Nat) : Nat :=
+    if it.atEnd then min
+    else if it.curr == '\n' then consumeSpaces it.next 0 min
+    else findNextLine it.next min
+
+private def removeNumLeadingSpaces (n : Nat) (s : String) : String :=
+  consumeSpaces n s.iter ""
+where
+  consumeSpaces (n : Nat) (it : String.Iterator) (r : String) : String :=
+     match n with
+     | 0 => saveLine it r
+     | n+1 =>
+       if it.atEnd then r
+       else if it.curr == ' ' || it.curr == '\t' then consumeSpaces n it.next r
+       else saveLine it r
+  termination_by (it, 1)
+  saveLine (it : String.Iterator) (r : String) : String :=
+    if it.atEnd then r
+    else if it.curr == '\n' then consumeSpaces n it.next (r.push '\n')
+    else saveLine it.next (r.push it.curr)
+  termination_by (it, 0)
+
+def removeLeadingSpaces (s : String) : String :=
+  let n := findLeadingSpacesSize s
+  if n == 0 then s else removeNumLeadingSpaces n s
+
 namespace Name
 
 def getRoot : Name → Name
@@ -909,11 +947,6 @@ def _root_.Substring.toName (s : Substring) : Name :=
       else
         Name.mkStr n comp
 
-/--
-Converts a `String` to a hierarchical `Name` after splitting it at the dots.
-
-`"a.b".toName` is the name `a.b`, not `«a.b»`. For the latter, use `Name.mkSimple`.
--/
 def _root_.String.toName (s : String) : Name :=
   s.toSubstring.toName
 
@@ -1194,6 +1227,14 @@ instance : Coe (Lean.Term) (Lean.TSyntax `Lean.Parser.Term.funBinder) where
 
 end Lean.Syntax
 
+set_option linter.unusedVariables.funArgs false in
+/--
+  Gadget for automatic parameter support. This is similar to the `optParam` gadget, but it uses
+  the given tactic.
+  Like `optParam`, this gadget only affects elaboration.
+  For example, the tactic will *not* be invoked during type class resolution. -/
+abbrev autoParam.{u} (α : Sort u) (tactic : Lean.Syntax) : Sort u := α
+
 /-! # Helper functions for manipulating interpolated strings -/
 
 namespace Lean.Syntax

src/Init/NotationExtra.lean

@@ -6,13 +6,15 @@ Authors: Leonardo de Moura
 Extra notation that depends on Init/Meta
 -/
 prelude
-import Init.Data.ToString.Basic
-import Init.Data.Array.Subarray
-import Init.Conv
 import Init.Meta
-
+import Init.Data.Array.Subarray
+import Init.Data.ToString
+import Init.Conv
 namespace Lean
 
+macro "Macro.trace[" id:ident "]" s:interpolatedStr(term) : term =>
+  `(Macro.trace $(quote id.getId.eraseMacroScopes) (s! $s))
+
 -- Auxiliary parsers and functions for declaring notation with binders
 
 syntax unbracketedExplicitBinders := (ppSpace binderIdent)+ (" : " term)?
@@ -222,35 +224,35 @@ macro tk:"calc" steps:calcSteps : conv =>
   | _ => throw ()
 
 @[app_unexpander Name.mkStr1] def unexpandMkStr1 : Lean.PrettyPrinter.Unexpander
-  | `($(_) $a:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit ("`" ++  a.getString)]
+  | `($(_) $a:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{a.getString}"]
   | _  => throw ()
 
 @[app_unexpander Name.mkStr2] def unexpandMkStr2 : Lean.PrettyPrinter.Unexpander
-  | `($(_) $a1:str $a2:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit ("`" ++ a1.getString ++ "." ++ a2.getString)]
+  | `($(_) $a1:str $a2:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{a1.getString}.{a2.getString}"]
   | _  => throw ()
 
 @[app_unexpander Name.mkStr3] def unexpandMkStr3 : Lean.PrettyPrinter.Unexpander
-  | `($(_) $a1:str $a2:str $a3:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit ("`" ++ a1.getString ++ "." ++ a2.getString ++ "." ++ a3.getString)]
+  | `($(_) $a1:str $a2:str $a3:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{a1.getString}.{a2.getString}.{a3.getString}"]
   | _  => throw ()
 
 @[app_unexpander Name.mkStr4] def unexpandMkStr4 : Lean.PrettyPrinter.Unexpander
-  | `($(_) $a1:str $a2:str $a3:str $a4:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit ("`" ++ a1.getString ++ "." ++ a2.getString ++ "." ++ a3.getString ++ "." ++ a4.getString)]
+  | `($(_) $a1:str $a2:str $a3:str $a4:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{a1.getString}.{a2.getString}.{a3.getString}.{a4.getString}"]
   | _  => throw ()
 
 @[app_unexpander Name.mkStr5] def unexpandMkStr5 : Lean.PrettyPrinter.Unexpander
-  | `($(_) $a1:str $a2:str $a3:str $a4:str $a5:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit ("`" ++ a1.getString ++ "." ++ a2.getString ++ "." ++ a3.getString ++ "." ++ a4.getString ++ "." ++ a5.getString)]
+  | `($(_) $a1:str $a2:str $a3:str $a4:str $a5:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{a1.getString}.{a2.getString}.{a3.getString}.{a4.getString}.{a5.getString}"]
   | _  => throw ()
 
 @[app_unexpander Name.mkStr6] def unexpandMkStr6 : Lean.PrettyPrinter.Unexpander
-  | `($(_) $a1:str $a2:str $a3:str $a4:str $a5:str $a6:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit ("`" ++ a1.getString ++ "." ++ a2.getString ++ "." ++ a3.getString ++ "." ++ a4.getString ++ "." ++ a5.getString ++ "." ++ a6.getString)]
+  | `($(_) $a1:str $a2:str $a3:str $a4:str $a5:str $a6:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{a1.getString}.{a2.getString}.{a3.getString}.{a4.getString}.{a5.getString}.{a6.getString}"]
   | _  => throw ()
 
 @[app_unexpander Name.mkStr7] def unexpandMkStr7 : Lean.PrettyPrinter.Unexpander
-  | `($(_) $a1:str $a2:str $a3:str $a4:str $a5:str $a6:str $a7:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit ("`" ++ a1.getString ++ "." ++ a2.getString ++ "." ++ a3.getString ++ "." ++ a4.getString ++ "." ++ a5.getString ++ "." ++ a6.getString ++ "." ++ a7.getString)]
+  | `($(_) $a1:str $a2:str $a3:str $a4:str $a5:str $a6:str $a7:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{a1.getString}.{a2.getString}.{a3.getString}.{a4.getString}.{a5.getString}.{a6.getString}.{a7.getString}"]
   | _  => throw ()
 
 @[app_unexpander Name.mkStr8] def unexpandMkStr8 : Lean.PrettyPrinter.Unexpander
-  | `($(_) $a1:str $a2:str $a3:str $a4:str $a5:str $a6:str $a7:str $a8:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit ("`" ++ a1.getString ++ "." ++ a2.getString ++ "." ++ a3.getString ++ "." ++ a4.getString ++ "." ++ a5.getString ++ "." ++ a6.getString ++ "." ++ a7.getString ++ "." ++ a8.getString)]
+  | `($(_) $a1:str $a2:str $a3:str $a4:str $a5:str $a6:str $a7:str $a8:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{a1.getString}.{a2.getString}.{a3.getString}.{a4.getString}.{a5.getString}.{a6.getString}.{a7.getString}.{a8.getString}"]
   | _  => throw ()
 
 @[app_unexpander Array.empty] def unexpandArrayEmpty : Lean.PrettyPrinter.Unexpander

src/Init/Omega/Int.lean

@@ -50,9 +50,6 @@ theorem ofNat_shiftLeft_eq {x y : Nat} : (x <<< y : Int) = (x : Int) * (2 ^ y :
 theorem ofNat_shiftRight_eq_div_pow {x y : Nat} : (x >>> y : Int) = (x : Int) / (2 ^ y : Nat) := by
   simp only [Nat.shiftRight_eq_div_pow, Int.ofNat_ediv]
 
-theorem emod_ofNat_nonneg {x : Nat} {y : Int} : 0 ≤ (x : Int) % y :=
-  Int.ofNat_zero_le _
-
 -- FIXME these are insane:
 theorem lt_of_not_ge {x y : Int} (h : ¬ (x ≤ y)) : y < x := Int.not_le.mp h
 theorem lt_of_not_le {x y : Int} (h : ¬ (x ≤ y)) : y < x := Int.not_le.mp h
@@ -137,13 +134,11 @@ theorem add_le_iff_le_sub (a b c : Int) : a + b ≤ c ↔ a ≤ c - b := by
     lhs
     rw [← Int.add_zero c, ← Int.sub_self (-b), Int.sub_eq_add_neg, ← Int.add_assoc, Int.neg_neg,
       Int.add_le_add_iff_right]
-  try rfl -- stage0 update TODO: Change this to rfl or remove
 
 theorem le_add_iff_sub_le (a b c : Int) : a ≤ b + c ↔ a - c ≤ b := by
   conv =>
     lhs
     rw [← Int.neg_neg c, ← Int.sub_eq_add_neg, ← add_le_iff_le_sub]
-  try rfl -- stage0 update TODO: Change this to rfl or remove
 
 theorem add_le_zero_iff_le_neg (a b : Int) : a + b ≤ 0 ↔ a ≤ - b := by
   rw [add_le_iff_le_sub, Int.zero_sub]

src/Init/Omega/LinearCombo.lean

@@ -5,7 +5,6 @@ Authors: Scott Morrison
 -/
 prelude
 import Init.Omega.Coeffs
-import Init.Data.ToString.Macro
 
 /-!
 # Linear combinations

src/Init/Prelude.lean

@@ -488,7 +488,6 @@ attribute [unbox] Prod
 Similar to `Prod`, but `α` and `β` can be propositions.
 We use this type internally to automatically generate the `brecOn` recursor.
 -/
-@[pp_using_anonymous_constructor]
 structure PProd (α : Sort u) (β : Sort v) where
   /-- The first projection out of a pair. if `p : PProd α β` then `p.1 : α`. -/
   fst : α
@@ -510,7 +509,6 @@ structure MProd (α β : Type u) where
 constructed and destructed like a pair: if `ha : a` and `hb : b` then
 `⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`.
 -/
-@[pp_using_anonymous_constructor]
 structure And (a b : Prop) : Prop where
   /-- `And.intro : a → b → a ∧ b` is the constructor for the And operation. -/
   intro ::
@@ -577,7 +575,6 @@ a pair-like type, so if you have `x : α` and `h : p x` then
 `⟨x, h⟩ : {x // p x}`. An element `s : {x // p x}` will coerce to `α` but
 you can also make it explicit using `s.1` or `s.val`.
 -/
-@[pp_using_anonymous_constructor]
 structure Subtype {α : Sort u} (p : α → Prop) where
   /-- If `s : {x // p x}` then `s.val : α` is the underlying element in the base
   type. You can also write this as `s.1`, or simply as `s` when the type is
@@ -1197,12 +1194,7 @@ class HDiv (α : Type u) (β : Type v) (γ : outParam (Type w)) where
   /-- `a / b` computes the result of dividing `a` by `b`.
   The meaning of this notation is type-dependent.
   * For most types like `Nat`, `Int`, `Rat`, `Real`, `a / 0` is defined to be `0`.
-  * For `Nat`, `a / b` rounds downwards.
-  * For `Int`, `a / b` rounds downwards if `b` is positive or upwards if `b` is negative.
-    It is implemented as `Int.ediv`, the unique function satisfiying
-    `a % b + b * (a / b) = a` and `0 ≤ a % b < natAbs b` for `b ≠ 0`.
-    Other rounding conventions are available using the functions
-    `Int.fdiv` (floor rounding) and `Int.div` (truncation rounding).
+  * For `Nat` and `Int`, `a / b` rounds toward 0.
   * For `Float`, `a / 0` follows the IEEE 754 semantics for division,
     usually resulting in `inf` or `nan`. -/
   hDiv : α → β → γ
@@ -1214,8 +1206,7 @@ This enables the notation `a % b : γ` where `a : α`, `b : β`.
 class HMod (α : Type u) (β : Type v) (γ : outParam (Type w)) where
   /-- `a % b` computes the remainder upon dividing `a` by `b`.
   The meaning of this notation is type-dependent.
-  * For `Nat` and `Int` it satisfies `a % b + b * (a / b) = a`,
-    and `a % 0` is defined to be `a`. -/
+  * For `Nat` and `Int`, `a % 0` is defined to be `a`. -/
   hMod : α → β → γ
 
 /--
@@ -1818,7 +1809,6 @@ theorem System.Platform.numBits_eq : Or (Eq numBits 32) (Eq numBits 64) :=
 `Fin n` is a natural number `i` with the constraint that `0 ≤ i < n`.
 It is the "canonical type with `n` elements".
 -/
-@[pp_using_anonymous_constructor]
 structure Fin (n : Nat) where
   /-- If `i : Fin n`, then `i.val : ℕ` is the described number. It can also be
   written as `i.1` or just `i` when the target type is known. -/
@@ -2543,6 +2533,43 @@ def panic {α : Type u} [Inhabited α] (msg : String) : α :=
 -- TODO: this be applied directly to `Inhabited`'s definition when we remove the above workaround
 attribute [nospecialize] Inhabited
 
+/--
+The class `GetElem cont idx elem dom` implements the `xs[i]` notation.
+When you write this, given `xs : cont` and `i : idx`, Lean looks for an instance
+of `GetElem cont idx elem dom`. Here `elem` is the type of `xs[i]`, while
+`dom` is whatever proof side conditions are required to make this applicable.
+For example, the instance for arrays looks like
+`GetElem (Array α) Nat α (fun xs i => i < xs.size)`.
+
+The proof side-condition `dom xs i` is automatically dispatched by the
+`get_elem_tactic` tactic, which can be extended by adding more clauses to
+`get_elem_tactic_trivial`.
+-/
+class GetElem (cont : Type u) (idx : Type v) (elem : outParam (Type w)) (dom : outParam (cont → idx → Prop)) where
+  /--
+  The syntax `arr[i]` gets the `i`'th element of the collection `arr`.
+  If there are proof side conditions to the application, they will be automatically
+  inferred by the `get_elem_tactic` tactic.
+
+  The actual behavior of this class is type-dependent,
+  but here are some important implementations:
+  * `arr[i] : α` where `arr : Array α` and `i : Nat` or `i : USize`:
+    does array indexing with no bounds check and a proof side goal `i < arr.size`.
+  * `l[i] : α` where `l : List α` and `i : Nat`: index into a list,
+    with proof side goal `i < l.length`.
+  * `stx[i] : Syntax` where `stx : Syntax` and `i : Nat`: get a syntax argument,
+    no side goal (returns `.missing` out of range)
+
+  There are other variations on this syntax:
+  * `arr[i]`: proves the proof side goal by `get_elem_tactic`
+  * `arr[i]!`: panics if the side goal is false
+  * `arr[i]?`: returns `none` if the side goal is false
+  * `arr[i]'h`: uses `h` to prove the side goal
+  -/
+  getElem (xs : cont) (i : idx) (h : dom xs i) : elem
+
+export GetElem (getElem)
+
 /--
 `Array α` is the type of [dynamic arrays](https://en.wikipedia.org/wiki/Dynamic_array)
 with elements from `α`. This type has special support in the runtime.
@@ -2600,6 +2627,9 @@ def Array.get {α : Type u} (a : @& Array α) (i : @& Fin a.size) : α :=
 def Array.get! {α : Type u} [Inhabited α] (a : @& Array α) (i : @& Nat) : α :=
   Array.getD a i default
 
+instance : GetElem (Array α) Nat α fun xs i => LT.lt i xs.size where
+  getElem xs i h := xs.get ⟨i, h⟩
+
 /--
 Push an element onto the end of an array. This is amortized O(1) because
 `Array α` is internally a dynamic array.
@@ -2715,7 +2745,7 @@ def List.redLength : List α → Nat
 /-- Convert a `List α` into an `Array α`. This is O(n) in the length of the list.  -/
 -- This function is exported to C, where it is called by `Array.mk`
 -- (the constructor) to implement this functionality.
-@[inline, match_pattern, pp_nodot, export lean_list_to_array]
+@[inline, match_pattern, export lean_list_to_array]
 def List.toArray (as : List α) : Array α :=
   as.toArrayAux (Array.mkEmpty as.redLength)
 
@@ -3452,31 +3482,20 @@ instance : Hashable String where
 namespace Lean
 
 /--
-Hierarchical names consist of a sequence of components, each of
-which is either a string or numeric, that are written separated by dots (`.`).
+Hierarchical names. We use hierarchical names to name declarations and
+for creating unique identifiers for free variables and metavariables.
 
-Hierarchical names are used to name declarations and for creating
-unique identifiers for free variables and metavariables.
-
-You can create hierarchical names using a backtick:
+You can create hierarchical names using the following quotation notation.
 ```
 `Lean.Meta.whnf
 ```
-It is short for `.str (.str (.str .anonymous "Lean") "Meta") "whnf"`.
-
-You can use double backticks to request Lean to statically check whether the name
+It is short for `.str (.str (.str .anonymous "Lean") "Meta") "whnf"`
+You can use double quotes to request Lean to statically check whether the name
 corresponds to a Lean declaration in scope.
 ```
 ``Lean.Meta.whnf
 ```
 If the name is not in scope, Lean will report an error.
-
-There are two ways to convert a `String` to a `Name`:
-
- 1. `Name.mkSimple` creates a name with a single string component.
-
- 2. `String.toName` first splits the string into its dot-separated
-    components, and then creates a hierarchical name.
 -/
 inductive Name where
   /-- The "anonymous" name. -/
@@ -3527,9 +3546,7 @@ abbrev mkNum (p : Name) (v : Nat) : Name :=
   Name.num p v
 
 /--
-Converts a `String` to a `Name` without performing any parsing. `mkSimple s` is short for `.str .anonymous s`.
-
-This means that `mkSimple "a.b"` is the name `«a.b»`, not `a.b`.
+Short for `.str .anonymous s`.
 -/
 abbrev mkSimple (s : String) : Name :=
   .str .anonymous s
@@ -3867,6 +3884,9 @@ def getArg (stx : Syntax) (i : Nat) : Syntax :=
   | Syntax.node _ _ args => args.getD i Syntax.missing
   | _                    => Syntax.missing
 
+instance : GetElem Syntax Nat Syntax fun _ _ => True where
+  getElem stx i _ := stx.getArg i
+
 /-- Gets the list of arguments of the syntax node, or `#[]` if it's not a `node`. -/
 def getArgs (stx : Syntax) : Array Syntax :=
   match stx with
@@ -4561,12 +4581,6 @@ def resolveNamespace (n : Name) : MacroM (List Name) := do
 Resolves the given name to an overload list of global definitions.
 The `List String` in each alternative is the deduced list of projections
 (which are ambiguous with name components).
-
-Remark: it will not trigger actions associated with reserved names. Recall that Lean
-has reserved names. For example, a definition `foo` has a reserved name `foo.def` for theorem
-containing stating that `foo` is equal to its definition. The action associated with `foo.def`
-automatically proves the theorem. At the macro level, the name is resolved, but the action is not
-executed. The actions are executed by the elaborator when converting `Syntax` into `Expr`.
 -/
 def resolveGlobalName (n : Name) : MacroM (List (Prod Name (List String))) := do
   (← getMethods).resolveGlobalName n

src/Init/PropLemmas.lean

@@ -21,7 +21,7 @@ set_option linter.missingDocs true -- keep it documented
   | rfl, rfl, _ => rfl
 
 @[simp] theorem eq_true_eq_id : Eq True = id := by
-  funext _; simp only [true_iff, id_def, eq_iff_iff]
+  funext _; simp only [true_iff, id.def, eq_iff_iff]
 
 theorem proof_irrel_heq {p q : Prop} (hp : p) (hq : q) : HEq hp hq := by
   cases propext (iff_of_true hp hq); rfl

src/Init/RCases.lean

@@ -5,8 +5,7 @@ Authors: Mario Carneiro, Jacob von Raumer
 -/
 prelude
 import Init.Tactics
-import Init.Meta
-
+import Init.NotationExtra
 
 /-!
 # Recursive cases (`rcases`) tactic and related tactics
@@ -128,7 +127,7 @@ the input expression). An `rcases` pattern has the following grammar:
   and so on.
 * A `@` before a tuple pattern as in `@⟨p1, p2, p3⟩` will bind all arguments in the constructor,
   while leaving the `@` off will only use the patterns on the explicit arguments.
-* An alternation pattern `p1 | p2 | p3`, which matches an inductive type with multiple constructors,
+* An alteration pattern `p1 | p2 | p3`, which matches an inductive type with multiple constructors,
   or a nested disjunction like `a ∨ b ∨ c`.
 
 A pattern like `⟨a, b, c⟩ | ⟨d, e⟩` will do a split over the inductive datatype,

src/Init/Simproc.lean

@@ -11,23 +11,22 @@ namespace Lean.Parser
 A user-defined simplification procedure used by the `simp` tactic, and its variants.
 Here is an example.
 ```lean
-theorem and_false_eq {p : Prop} (q : Prop) (h : p = False) : (p ∧ q) = False := by simp [*]
-
-open Lean Meta Simp
-simproc ↓ shortCircuitAnd (And _ _) := fun e => do
-  let_expr And p q := e | return .continue
-  let r ← simp p
-  let_expr False := r.expr | return .continue
-  let proof ← mkAppM ``and_false_eq #[q, (← r.getProof)]
-  return .done { expr := r.expr, proof? := some proof }
+simproc reduce_add (_ + _) := fun e => do
+  unless (e.isAppOfArity ``HAdd.hAdd 6) do return none
+  let some n ← getNatValue? (e.getArg! 4) | return none
+  let some m ← getNatValue? (e.getArg! 5) | return none
+  return some (.done { expr := mkNatLit (n+m) })
 ```
-The `simp` tactic invokes `shortCircuitAnd` whenever it finds a term of the form `And _ _`.
+The `simp` tactic invokes `reduce_add` whenever it finds a term of the form `_ + _`.
 The simplification procedures are stored in an (imperfect) discrimination tree.
 The procedure should **not** assume the term `e` perfectly matches the given pattern.
 The body of a simplification procedure must have type `Simproc`, which is an alias for
-`Expr → SimpM Step`
+`Expr → SimpM (Option Step)`.
 You can instruct the simplifier to apply the procedure before its sub-expressions
-have been simplified by using the modifier `↓` before the procedure name.
+have been simplified by using the modifier `↓` before the procedure name. Example.
+```lean
+simproc ↓ reduce_add (_ + _) := fun e => ...
+```
 Simplification procedures can be also scoped or local.
 -/
 syntax (docComment)? attrKind "simproc " (Tactic.simpPre <|> Tactic.simpPost)? ("[" ident,* "]")? ident " (" term ")" " := " term : command

src/Init/System/FilePath.lean

@@ -73,21 +73,7 @@ private def posOfLastSep (p : FilePath) : Option String.Pos :=
   p.toString.revFind pathSeparators.contains
 
 def parent (p : FilePath) : Option FilePath :=
-  let extractParentPath := FilePath.mk <$> p.toString.extract {} <$> posOfLastSep p
-  if p.isAbsolute then
-    let lengthOfRootDirectory := if pathSeparators.contains p.toString.front then 1 else 3
-    if p.toString.length == lengthOfRootDirectory then
-      -- `p` is a root directory
-      none
-    else if posOfLastSep p == String.Pos.mk (lengthOfRootDirectory - 1) then
-      -- `p` is a direct child of the root
-      some ⟨p.toString.extract 0 ⟨lengthOfRootDirectory⟩⟩
-    else
-      -- `p` is an absolute path with at least two subdirectories
-      extractParentPath
-  else
-    -- `p` is a relative path
-    extractParentPath
+  FilePath.mk <$> p.toString.extract {} <$> posOfLastSep p
 
 def fileName (p : FilePath) : Option String :=
   let lastPart := match posOfLastSep p with

src/Init/Tactics.lean

@@ -224,7 +224,7 @@ the first matching constructor, or else fails.
 syntax (name := constructor) "constructor" : tactic
 
 /--
-Applies the first constructor when
+Applies the second constructor when
 the goal is an inductive type with exactly two constructors, or fails otherwise.
 ```
 example : True ∨ False := by
@@ -354,9 +354,6 @@ macro:1 x:tactic tk:" <;> " y:tactic:2 : tactic => `(tactic|
     with_annotate_state $tk skip
     all_goals $y:tactic)
 
-/-- `fail msg` is a tactic that always fails, and produces an error using the given message. -/
-syntax (name := fail) "fail" (ppSpace str)? : tactic
-
 /-- `eq_refl` is equivalent to `exact rfl`, but has a few optimizations. -/
 syntax (name := eqRefl) "eq_refl" : tactic
 
@@ -368,23 +365,10 @@ for new reflexive relations.
 Remark: `rfl` is an extensible tactic. We later add `macro_rules` to try different
 reflexivity theorems (e.g., `Iff.rfl`).
 -/
-macro "rfl" : tactic => `(tactic| fail "The rfl tactic failed. Possible reasons:
-- The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma).
-- The arguments of the relation are not equal.
-Try using the reflexivitiy lemma for your relation explicitly, e.g. `exact Eq.rfl`.")
+macro "rfl" : tactic => `(tactic| eq_refl)
 
-macro_rules | `(tactic| rfl) => `(tactic| eq_refl)
 macro_rules | `(tactic| rfl) => `(tactic| exact HEq.rfl)
 
-/--
-This tactic applies to a goal whose target has the form `x ~ x`,
-where `~` is a reflexive relation other than `=`,
-that is, a relation which has a reflexive lemma tagged with the attribute @[refl].
--/
-syntax (name := applyRfl) "apply_rfl" : tactic
-
-macro_rules | `(tactic| rfl) => `(tactic| apply_rfl)
-
 /--
 `rfl'` is similar to `rfl`, but disables smart unfolding and unfolds all kinds of definitions,
 theorems included (relevant for declarations defined by well-founded recursion).
@@ -915,6 +899,9 @@ example : ∀ x : Nat, x = x := by unhygienic
 -/
 macro "unhygienic " t:tacticSeq : tactic => `(tactic| set_option tactic.hygienic false in $t)
 
+/-- `fail msg` is a tactic that always fails, and produces an error using the given message. -/
+syntax (name := fail) "fail" (ppSpace str)? : tactic
+
 /--
 `checkpoint tac` acts the same as `tac`, but it caches the input and output of `tac`,
 and if the file is re-elaborated and the input matches, the tactic is not re-run and
@@ -1323,22 +1310,6 @@ used when closing the goal.
 -/
 syntax (name := apply?) "apply?" (" using " (colGt term),+)? : tactic
 
-/--
-Syntax for excluding some names, e.g. `[-my_lemma, -my_theorem]`.
--/
-syntax rewrites_forbidden := " [" (("-" ident),*,?) "]"
-
-/--
-`rw?` tries to find a lemma which can rewrite the goal.
-
-`rw?` should not be left in proofs; it is a search tool, like `apply?`.
-
-Suggestions are printed as `rw [h]` or `rw [← h]`.
-
-You can use `rw? [-my_lemma, -my_theorem]` to prevent `rw?` using the named lemmas.
--/
-syntax (name := rewrites?) "rw?" (ppSpace location)? (rewrites_forbidden)? : tactic
-
 /--
 `show_term tac` runs `tac`, then prints the generated term in the form
 "exact X Y Z" or "refine X ?_ Z" if there are remaining subgoals.
@@ -1522,16 +1493,16 @@ macro "get_elem_tactic" : tactic =>
   - Use `a[i]'h` notation instead, where `h` is a proof that index is valid"
    )
 
+@[inherit_doc getElem]
+syntax:max term noWs "[" withoutPosition(term) "]" : term
+macro_rules | `($x[$i]) => `(getElem $x $i (by get_elem_tactic))
+
+@[inherit_doc getElem]
+syntax term noWs "[" withoutPosition(term) "]'" term:max : term
+macro_rules | `($x[$i]'$h) => `(getElem $x $i $h)
+
 /--
 Searches environment for definitions or theorems that can be substituted in
 for `exact?% to solve the goal.
  -/
 syntax (name := Lean.Parser.Syntax.exact?) "exact?%" : term
-
-set_option linter.unusedVariables.funArgs false in
-/--
-  Gadget for automatic parameter support. This is similar to the `optParam` gadget, but it uses
-  the given tactic.
-  Like `optParam`, this gadget only affects elaboration.
-  For example, the tactic will *not* be invoked during type class resolution. -/
-abbrev autoParam.{u} (α : Sort u) (tactic : Lean.Syntax) : Sort u := α

src/Init/Util.lean

@@ -73,6 +73,19 @@ def withPtrEq {α : Type u} (a b : α) (k : Unit → Bool) (h : a = b → k () =
 @[implemented_by withPtrAddrUnsafe]
 def withPtrAddr {α : Type u} {β : Type v} (a : α) (k : USize → β) (h : ∀ u₁ u₂, k u₁ = k u₂) : β := k 0
 
+@[never_extract]
+private def outOfBounds [Inhabited α] : α :=
+  panic! "index out of bounds"
+
+@[inline] def getElem! [GetElem cont idx elem dom] [Inhabited elem] (xs : cont) (i : idx) [Decidable (dom xs i)] : elem :=
+  if h : _ then getElem xs i h else outOfBounds
+
+@[inline] def getElem? [GetElem cont idx elem dom] (xs : cont) (i : idx) [Decidable (dom xs i)] : Option elem :=
+  if h : _ then some (getElem xs i h) else none
+
+macro:max x:term noWs "[" i:term "]" noWs "?" : term => `(getElem? $x $i)
+macro:max x:term noWs "[" i:term "]" noWs "!" : term => `(getElem! $x $i)
+
 /--
   Marks given value and its object graph closure as multi-threaded if currently
   marked single-threaded. This will make reference counter updates atomic and

src/Lean.lean

@@ -24,7 +24,6 @@ import Lean.Eval
 import Lean.Structure
 import Lean.PrettyPrinter
 import Lean.CoreM
-import Lean.ReservedNameAction
 import Lean.InternalExceptionId
 import Lean.Server
 import Lean.ScopedEnvExtension

src/Lean/AuxRecursor.lean

@@ -34,7 +34,7 @@ def isAuxRecursor (env : Environment) (declName : Name) : Bool :=
   || declName == ``Eq.ndrec
   || declName == ``Eq.ndrecOn
 
-def isAuxRecursorWithSuffix (env : Environment) (declName : Name) (suffix : String) : Bool :=
+def isAuxRecursorWithSuffix (env : Environment) (declName : Name) (suffix : Name) : Bool :=
   match declName with
   | .str _ s => s == suffix && isAuxRecursor env declName
   | _ => false

src/Lean/Compiler/IR/EmitLLVM.lean

@@ -147,7 +147,7 @@ def callLeanRefcountFn (builder : LLVM.Builder llvmctx)
     (delta : Option (LLVM.Value llvmctx) := Option.none) : M llvmctx Unit := do
   let fnName :=  s!"lean_{kind}{if checkRef? then "" else "_ref"}{if delta.isNone then "" else "_n"}"
   let retty ← LLVM.voidType llvmctx
-  let argtys ← if delta.isNone then pure #[← LLVM.voidPtrType llvmctx] else pure #[← LLVM.voidPtrType llvmctx, ← LLVM.size_tType llvmctx]
+  let argtys := if delta.isNone then #[← LLVM.voidPtrType llvmctx] else #[← LLVM.voidPtrType llvmctx, ← LLVM.size_tType llvmctx]
   let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys
   let fnty ← LLVM.functionType retty argtys
   match delta with
@@ -663,7 +663,7 @@ def emitExternCall (builder : LLVM.Builder llvmctx)
     (name : String := "") : M llvmctx (LLVM.Value llvmctx) :=
   match getExternEntryFor extData `c with
   | some (ExternEntry.standard _ extFn) => emitSimpleExternalCall builder extFn ps ys retty name
-  | some (ExternEntry.inline `llvm _pat) => throw "Unimplemented codegen of inline LLVM"
+  | some (ExternEntry.inline "llvm" _pat) => throw "Unimplemented codegen of inline LLVM"
   | some (ExternEntry.inline _ pat) => throw s!"Cannot codegen non-LLVM inline code '{pat}'."
   | some (ExternEntry.foreign _ extFn)  => emitSimpleExternalCall builder extFn ps ys retty name
   | _ => throw s!"Failed to emit extern application '{f}'."

src/Lean/Compiler/ImplementedByAttr.lean

@@ -17,7 +17,7 @@ builtin_initialize implementedByAttr : ParametricAttribute Name ← registerPara
   getParam := fun declName stx => do
     let decl ← getConstInfo declName
     let fnNameStx ← Attribute.Builtin.getIdent stx
-    let fnName ← Elab.realizeGlobalConstNoOverloadWithInfo fnNameStx
+    let fnName ← Elab.resolveGlobalConstNoOverloadWithInfo fnNameStx
     let fnDecl ← getConstInfo fnName
     unless decl.levelParams.length == fnDecl.levelParams.length do
       throwError "invalid 'implemented_by' argument '{fnName}', '{fnName}' has {fnDecl.levelParams.length} universe level parameter(s), but '{declName}' has {decl.levelParams.length}"

src/Lean/Compiler/InitAttr.lean

@@ -44,7 +44,7 @@ unsafe def registerInitAttrUnsafe (attrName : Name) (runAfterImport : Bool) (ref
       let decl ← getConstInfo declName
       match (← Attribute.Builtin.getIdent? stx) with
       | some initFnName =>
-        let initFnName ← Elab.realizeGlobalConstNoOverloadWithInfo initFnName
+        let initFnName ← Elab.resolveGlobalConstNoOverloadWithInfo initFnName
         let initDecl ← getConstInfo initFnName
         match getIOTypeArg initDecl.type with
         | none => throwError "initialization function '{initFnName}' must have type of the form `IO <type>`"

src/Lean/Compiler/LCNF/JoinPoints.lean

@@ -346,7 +346,7 @@ We call this whenever we enter a new local function. It clears both the
 current join point and the list of candidates since we can't lift join
 points outside of functions as explained in `mergeJpContextIfNecessary`.
 -/
-def withNewFunScope (x : ExtendM α): ExtendM α := do
+def withNewFunScope (decl : FunDecl) (x : ExtendM α): ExtendM α := do
   withReader (fun ctx => { ctx with currentJp? := none, candidates := {} }) do
     withNewScope do
       x
@@ -412,7 +412,7 @@ where
       withNewCandidate decl.fvarId do
         return Code.updateFun! code decl (← go k)
     | .fun decl k =>
-      let decl ← withNewFunScope do
+      let decl ← withNewFunScope decl do
         decl.updateValue (← go decl.value)
       withNewCandidate decl.fvarId do
         return Code.updateFun! code decl (← go k)

src/Lean/Compiler/LCNF/LambdaLifting.lean

@@ -88,7 +88,7 @@ occurring in `decl`.
 -/
 def mkAuxDecl (closure : Array Param) (decl : FunDecl) : LiftM LetDecl := do
   let nameNew ← mkAuxDeclName
-  let inlineAttr? ← if (← read).inheritInlineAttrs then pure (← read).mainDecl.inlineAttr? else pure none
+  let inlineAttr? := if (← read).inheritInlineAttrs then (← read).mainDecl.inlineAttr? else none
   let auxDecl ← go nameNew (← read).mainDecl.safe inlineAttr? |>.run' {}
   let us := auxDecl.levelParams.map mkLevelParam
   let auxDeclName ← match (← cacheAuxDecl auxDecl) with

src/Lean/CoreM.lean

@@ -219,7 +219,7 @@ def checkMaxHeartbeatsCore (moduleName : String) (optionName : Name) (max : Nat)
   unless max == 0 do
     let numHeartbeats ← IO.getNumHeartbeats
     if numHeartbeats - (← read).initHeartbeats > max then
-      throwMaxHeartbeat (.mkSimple moduleName) optionName max
+      throwMaxHeartbeat moduleName optionName max
 
 def checkMaxHeartbeats (moduleName : String) : CoreM Unit := do
   checkMaxHeartbeatsCore moduleName `maxHeartbeats (← read).maxHeartbeats

src/Lean/Data/HashMap.lean

@@ -212,8 +212,6 @@ def insertIfNew (m : HashMap α β) (a : α) (b : β) : HashMap α β × Option
 instance : GetElem (HashMap α β) α (Option β) fun _ _ => True where
   getElem m k _ := m.find? k
 
-instance : LawfulGetElem (HashMap α β) α (Option β) fun _ _ => True where
-
 @[inline] def contains (m : HashMap α β) (a : α) : Bool :=
   match m with
   | ⟨ m, _ ⟩ => m.contains a

src/Lean/Data/Json/Basic.lean

@@ -10,8 +10,6 @@ import Init.Data.Range
 import Init.Data.OfScientific
 import Init.Data.Hashable
 import Lean.Data.RBMap
-import Init.Data.ToString.Macro
-
 namespace Lean
 
 -- mantissa * 10^-exponent

src/Lean/Data/JsonRpc.lean

@@ -183,9 +183,6 @@ structure ResponseError (α : Type u) where
 instance [ToJson α] : CoeOut (ResponseError α) Message :=
   ⟨fun r => Message.responseError r.id r.code r.message (r.data?.map toJson)⟩
 
-instance : CoeOut (ResponseError Unit) Message :=
-  ⟨fun r => Message.responseError r.id r.code r.message none⟩
-
 instance : Coe String RequestID := ⟨RequestID.str⟩
 instance : Coe JsonNumber RequestID := ⟨RequestID.num⟩
 

src/Lean/Data/Lsp/Basic.lean

@@ -52,7 +52,7 @@ instance : LE Range := leOfOrd
 structure Location where
   uri : DocumentUri
   range : Range
-  deriving Inhabited, BEq, ToJson, FromJson, Ord
+  deriving Inhabited, BEq, ToJson, FromJson
 
 structure LocationLink where
   originSelectionRange? : Option Range

src/Lean/Data/Lsp/Diagnostics.lean

@@ -25,7 +25,7 @@ open Json
 
 inductive DiagnosticSeverity where
   | error | warning | information | hint
-  deriving Inhabited, BEq, Ord
+  deriving Inhabited, BEq
 
 instance : FromJson DiagnosticSeverity := ⟨fun j =>
   match j.getNat? with
@@ -45,7 +45,7 @@ instance : ToJson DiagnosticSeverity := ⟨fun
 inductive DiagnosticCode where
   | int (i : Int)
   | string (s : String)
-  deriving Inhabited, BEq, Ord
+  deriving Inhabited, BEq
 
 instance : FromJson DiagnosticCode := ⟨fun
   | num (i : Int) => return DiagnosticCode.int i
@@ -62,7 +62,7 @@ inductive DiagnosticTag where
   | unnecessary
   /-- Deprecated or obsolete code. Rendered with a strike-through. -/
   | deprecated
-  deriving Inhabited, BEq, Ord
+  deriving Inhabited, BEq
 
 instance : FromJson DiagnosticTag := ⟨fun j =>
   match j.getNat? with
@@ -80,7 +80,7 @@ instance : ToJson DiagnosticTag := ⟨fun
 structure DiagnosticRelatedInformation where
   location : Location
   message : String
-  deriving Inhabited, BEq, ToJson, FromJson, Ord
+  deriving Inhabited, BEq, ToJson, FromJson
 
 /-- Represents a diagnostic, such as a compiler error or warning. Diagnostic objects are only valid in the scope of a resource.
 
@@ -113,29 +113,6 @@ structure DiagnosticWith (α : Type) where
 def DiagnosticWith.fullRange (d : DiagnosticWith α) : Range :=
   d.fullRange?.getD d.range
 
-local instance [Ord α] : Ord (Array α) := Ord.arrayOrd
-
-/-- Restriction of `DiagnosticWith` to properties that are displayed to users in the InfoView. -/
-private structure DiagnosticWith.UserVisible (α : Type) where
-  range               : Range
-  fullRange?          : Option Range
-  severity?           : Option DiagnosticSeverity
-  code?               : Option DiagnosticCode
-  source?             : Option String
-  message             : α
-  tags?               : Option (Array DiagnosticTag)
-  relatedInformation? : Option (Array DiagnosticRelatedInformation)
-  deriving Ord
-
-/-- Extracts user-visible properties from the given `DiagnosticWith`. -/
-private def DiagnosticWith.UserVisible.ofDiagnostic (d : DiagnosticWith α)
-    : DiagnosticWith.UserVisible α :=
-  { d with }
-
-/-- Compares `DiagnosticWith` instances modulo non-user-facing properties. -/
-def compareByUserVisible [Ord α] (a b : DiagnosticWith α) : Ordering :=
-  compare (DiagnosticWith.UserVisible.ofDiagnostic a) (DiagnosticWith.UserVisible.ofDiagnostic b)
-
 abbrev Diagnostic := DiagnosticWith String
 
 /-- Parameters for the [`textDocument/publishDiagnostics` notification](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#textDocument_publishDiagnostics). -/

src/Lean/Data/Lsp/Internal.lean

@@ -24,50 +24,44 @@ Identifier of a reference.
 -/
 inductive RefIdent where
   /-- Named identifier. These are used in all references that are globally available. -/
-  | const (moduleName : Name) (identName : Name) : RefIdent
+  | const : Name → RefIdent
   /-- Unnamed identifier. These are used for all local references. -/
-  | fvar (moduleName : Name) (id : FVarId) : RefIdent
+  | fvar  : FVarId → RefIdent
   deriving BEq, Hashable, Inhabited
 
 namespace RefIdent
 
-instance : ToJson FVarId where
-  toJson id := toJson id.name
+/-- Converts the reference identifier to a string by prefixing it with a symbol. -/
+def toString : RefIdent → String
+  | RefIdent.const n => s!"c:{n}"
+  | RefIdent.fvar id => s!"f:{id.name}"
 
-instance : FromJson FVarId where
-  fromJson? s := return ⟨← fromJson? s⟩
-
-/-- Shortened representation of `RefIdent` for more compact serialization. -/
-inductive RefIdentJsonRepr
-  /-- Shortened representation of `RefIdent.const` for more compact serialization. -/
-  | c (m n : Name)
-  /-- Shortened representation of `RefIdent.fvar` for more compact serialization. -/
-  | f (m : Name) (i : FVarId)
-  deriving FromJson, ToJson
-
-/-- Converts `id` to its compact serialization representation. -/
-def toJsonRepr : (id : RefIdent) → RefIdentJsonRepr
-  | const moduleName identName => .c moduleName identName
-  | fvar moduleName id => .f moduleName id
-
-/-- Converts `repr` to `RefIdent`. -/
-def fromJsonRepr : (repr : RefIdentJsonRepr) → RefIdent
-  | .c m n => const m n
-  | .f m i => fvar m i
-
-/-- Converts `RefIdent` from a JSON for `RefIdentJsonRepr`. -/
-def fromJson? (s : Json) : Except String RefIdent :=
-  return fromJsonRepr (← Lean.FromJson.fromJson? s)
-
-/-- Converts `RefIdent` to a JSON for `RefIdentJsonRepr`. -/
-def toJson (id : RefIdent) : Json :=
-  Lean.ToJson.toJson <| toJsonRepr id
+/--
+Converts the string representation of a reference identifier back to a reference identifier.
+The string representation must have been created by `RefIdent.toString`.
+-/
+def fromString (s : String) : Except String RefIdent := do
+  let sPrefix := s.take 2
+  let sName := s.drop 2
+  -- See `FromJson Name`
+  let name ← match sName with
+    | "[anonymous]" => pure Name.anonymous
+    | _ =>
+      let n := sName.toName
+      if n.isAnonymous then throw s!"expected a Name, got {sName}"
+      else pure n
+  match sPrefix with
+    | "c:" => return RefIdent.const name
+    | "f:" => return RefIdent.fvar <| FVarId.mk name
+    | _ => throw "string must start with 'c:' or 'f:'"
 
 instance : FromJson RefIdent where
-  fromJson? := fromJson?
+  fromJson?
+    | (s : String) => fromString s
+    | j => Except.error s!"expected a String, got {j}"
 
 instance : ToJson RefIdent where
-  toJson := toJson
+  toJson ident := toString ident
 
 end RefIdent
 
@@ -90,7 +84,6 @@ structure RefInfo.Location where
   range       : Lsp.Range
   /-- Parent declaration of the reference. `none` if the reference is itself a declaration. -/
   parentDecl? : Option RefInfo.ParentDecl
-deriving Inhabited
 
 /-- Definition site and usage sites of a reference. Obtained from `Lean.Server.RefInfo`. -/
 structure RefInfo where
@@ -153,18 +146,17 @@ instance : FromJson RefInfo where
 def ModuleRefs := HashMap RefIdent RefInfo
 
 instance : ToJson ModuleRefs where
-  toJson m := Json.mkObj <| m.toList.map fun (ident, info) => (ident.toJson.compress, toJson info)
+  toJson m := Json.mkObj <| m.toList.map fun (ident, info) => (ident.toString, toJson info)
 
 instance : FromJson ModuleRefs where
   fromJson? j := do
     let node ← j.getObj?
     node.foldM (init := HashMap.empty) fun m k v =>
-      return m.insert (← RefIdent.fromJson? (← Json.parse k)) (← fromJson? v)
+      return m.insert (← RefIdent.fromString k) (← fromJson? v)
 
-/--
-Used in the `$/lean/ileanInfoUpdate` and `$/lean/ileanInfoFinal` watchdog <- worker notifications.
-Contains the definitions and references of the file managed by a worker.
--/
+/-- `$/lean/ileanInfoUpdate` and `$/lean/ileanInfoFinal` watchdog<-worker notifications.
+
+Contains the file's definitions and references. -/
 structure LeanIleanInfoParams where
   /-- Version of the file these references are from. -/
   version    : Nat
@@ -172,22 +164,4 @@ structure LeanIleanInfoParams where
   references : ModuleRefs
   deriving FromJson, ToJson
 
-/--
-Used in the `$/lean/importClosure` watchdog <- worker notification.
-Contains the full import closure of the file managed by a worker.
--/
-structure LeanImportClosureParams where
-  /-- Full import closure of the file. -/
-  importClosure : Array DocumentUri
-  deriving FromJson, ToJson
-
-/--
-Used in the `$/lean/importClosure` watchdog -> worker notification.
-Informs the worker that one of its dependencies has gone stale and likely needs to be rebuilt.
--/
-structure LeanStaleDependencyParams where
-  /-- The dependency that is stale. -/
-  staleDependency : DocumentUri
-  deriving FromJson, ToJson
-
 end Lean.Lsp

src/Lean/Data/Lsp/Ipc.lean

@@ -64,10 +64,9 @@ def readRequestAs (expectedMethod : String) (α) [FromJson α] : IpcM (Request
   (←stdout).readLspRequestAs expectedMethod α
 
 /--
-Reads response, discarding notifications and server-to-client requests in between.
-This function is meant purely for testing where we use `collectDiagnostics` explicitly
-if we do care about such notifications.
--/
+  Reads response, discarding notifications in between. This function is meant
+  purely for testing where we use `collectDiagnostics` explicitly if we do care
+  about such notifications. -/
 partial def readResponseAs (expectedID : RequestID) (α) [FromJson α] :
     IpcM (Response α) := do
   let m ← (←stdout).readLspMessage
@@ -80,28 +79,20 @@ partial def readResponseAs (expectedID : RequestID) (α) [FromJson α] :
     else
       throw $ userError s!"Expected id {expectedID}, got id {id}"
   | .notification .. => readResponseAs expectedID α
-  | .request .. => readResponseAs expectedID α
-  | .responseError .. => throw $ userError s!"Expected JSON-RPC response, got: '{(toJson m).compress}'"
+  | _ => throw $ userError s!"Expected JSON-RPC response, got: '{(toJson m).compress}'"
 
 def waitForExit : IpcM UInt32 := do
   (←read).wait
 
-/--
-Waits for the worker to emit all diagnostic notifications for the current document version and
-returns the last notification, if any.
-
-We used to return all notifications but with debouncing in the server, this would not be
-deterministic anymore as what messages are dropped depends on wall-clock timing.
- -/
+/-- Waits for the worker to emit all diagnostics for the current document version
+and returns them as a list. -/
 partial def collectDiagnostics (waitForDiagnosticsId : RequestID := 0) (target : DocumentUri) (version : Nat)
-: IpcM (Option (Notification PublishDiagnosticsParams)) := do
+: IpcM (List (Notification PublishDiagnosticsParams)) := do
   writeRequest ⟨waitForDiagnosticsId, "textDocument/waitForDiagnostics", WaitForDiagnosticsParams.mk target version⟩
-  loop
-where
-  loop := do
+  let rec loop : IpcM (List (Notification PublishDiagnosticsParams)) := do
     match (←readMessage) with
     | Message.response id _ =>
-      if id == waitForDiagnosticsId then return none
+      if id == waitForDiagnosticsId then return []
       else loop
     | Message.responseError id _    msg _ =>
       if id == waitForDiagnosticsId then
@@ -109,9 +100,10 @@ where
       else loop
     | Message.notification "textDocument/publishDiagnostics" (some param) =>
       match fromJson? (toJson param) with
-      | Except.ok diagnosticParam => return (← loop).getD ⟨"textDocument/publishDiagnostics", diagnosticParam⟩
+      | Except.ok diagnosticParam => return ⟨"textDocument/publishDiagnostics", diagnosticParam⟩ :: (←loop)
       | Except.error inner => throw $ userError s!"Cannot decode publishDiagnostics parameters\n{inner}"
     | _ => loop
+  loop
 
 def runWith (lean : System.FilePath) (args : Array String := #[]) (test : IpcM α) : IO α := do
   let proc ← Process.spawn {

src/Lean/Data/Lsp/TextSync.lean

@@ -38,7 +38,7 @@ structure DidOpenTextDocumentParams where
 
 structure TextDocumentChangeRegistrationOptions where
   documentSelector? : Option DocumentSelector := none
-  syncKind          : TextDocumentSyncKind
+  syncKind : TextDocumentSyncKind
   deriving FromJson
 
 inductive TextDocumentContentChangeEvent where
@@ -61,18 +61,13 @@ instance TextDocumentContentChangeEvent.hasToJson : ToJson TextDocumentContentCh
     | TextDocumentContentChangeEvent.fullChange text => [⟨"text", toJson text⟩]⟩
 
 structure DidChangeTextDocumentParams where
-  textDocument   : VersionedTextDocumentIdentifier
+  textDocument : VersionedTextDocumentIdentifier
   contentChanges : Array TextDocumentContentChangeEvent
   deriving ToJson, FromJson
 
-structure DidSaveTextDocumentParams where
-  textDocument : TextDocumentIdentifier
-  text?        : Option String
-  deriving ToJson, FromJson
-
 -- TODO: missing:
 -- WillSaveTextDocumentParams, TextDocumentSaveReason,
--- TextDocumentSaveRegistrationOptions
+-- TextDocumentSaveRegistrationOptions, DidSaveTextDocumentParams
 
 structure SaveOptions where
   includeText : Bool
@@ -86,11 +81,11 @@ structure DidCloseTextDocumentParams where
 
 /-- NOTE: This is defined twice in the spec. The latter version has more fields. -/
 structure TextDocumentSyncOptions where
-  openClose         : Bool
-  change            : TextDocumentSyncKind
-  willSave          : Bool
+  openClose : Bool
+  change : TextDocumentSyncKind
+  willSave : Bool
   willSaveWaitUntil : Bool
-  save?             : Option SaveOptions
+  save? : Option SaveOptions := none
   deriving ToJson, FromJson
 
 end Lsp

src/Lean/Data/Lsp/Window.lean

@@ -1,48 +0,0 @@
-/-
-Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Marc Huisinga
--/
-prelude
-import Lean.Data.Json
-
-open Lean
-
-inductive MessageType where
-  | error
-  | warning
-  | info
-  | log
-
-instance : FromJson MessageType where
-  fromJson?
-    | (1 : Nat) => .ok .error
-    | (2 : Nat) => .ok .warning
-    | (3 : Nat) => .ok .info
-    | (4 : Nat) => .ok .log
-    | _         => .error "Unknown MessageType ID"
-
-instance : ToJson MessageType where
-  toJson
-    | .error   => 1
-    | .warning => 2
-    | .info    => 3
-    | .log     => 4
-
-structure ShowMessageParams where
-  type    : MessageType
-  message : String
-  deriving FromJson, ToJson
-
-structure MessageActionItem where
-  title : String
-  deriving FromJson, ToJson
-
-structure ShowMessageRequestParams where
-  type     : MessageType
-  message  : String
-  actions? : Option (Array MessageActionItem)
-  deriving FromJson, ToJson
-
-def ShowMessageResponse := Option MessageActionItem
-  deriving FromJson, ToJson

src/Lean/Data/Name.lean

@@ -7,6 +7,8 @@ prelude
 import Init.Data.Ord
 namespace Lean
 
+instance : Coe String Name := ⟨Name.mkSimple⟩
+
 namespace Name
 -- Remark: we export the `Name.hash` to make sure it matches the hash implemented in C++
 @[export lean_name_hash_exported] def hashEx : Name → UInt64 :=

src/Lean/Data/NameMap.lean

@@ -11,6 +11,8 @@ import Lean.Data.SSet
 import Lean.Data.Name
 namespace Lean
 
+instance : Coe String Name := ⟨Name.mkSimple⟩
+
 def NameMap (α : Type) := RBMap Name α Name.quickCmp
 
 @[inline] def mkNameMap (α : Type) : NameMap α := mkRBMap Name α Name.quickCmp

src/Lean/Data/Parsec.lean

@@ -5,7 +5,7 @@ Author: Dany Fabian
 -/
 prelude
 import Init.NotationExtra
-import Init.Data.ToString.Macro
+import Init.Data.ToString.Basic
 
 namespace Lean
 

src/Lean/Data/PersistentArray.lean

@@ -6,7 +6,6 @@ Authors: Leonardo de Moura
 prelude
 import Init.Data.Array.Basic
 import Init.NotationExtra
-import Init.Data.ToString.Macro
 
 universe u v w
 
@@ -72,8 +71,6 @@ def get! [Inhabited α] (t : PersistentArray α) (i : Nat) : α :=
 instance [Inhabited α] : GetElem (PersistentArray α) Nat α fun as i => i < as.size where
   getElem xs i _ := xs.get! i
 
-instance [Inhabited α] : LawfulGetElem (PersistentArray α) Nat α fun as i => i < as.size where
-
 partial def setAux : PersistentArrayNode α → USize → USize → α → PersistentArrayNode α
   | node cs, i, shift, a =>
     let j     := div2Shift i shift

src/Lean/Data/PersistentHashMap.lean

@@ -5,7 +5,6 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Data.Array.BasicAux
-import Init.Data.ToString.Macro
 
 namespace Lean
 universe u v w w'
@@ -155,8 +154,6 @@ def find? {_ : BEq α} {_ : Hashable α} : PersistentHashMap α β → α → Op
 instance {_ : BEq α} {_ : Hashable α} : GetElem (PersistentHashMap α β) α (Option β) fun _ _ => True where
   getElem m i _ := m.find? i
 
-instance {_ : BEq α} {_ : Hashable α} : LawfulGetElem (PersistentHashMap α β) α (Option β) fun _ _ => True where
-
 @[inline] def findD {_ : BEq α} {_ : Hashable α} (m : PersistentHashMap α β) (a : α) (b₀ : β) : β :=
   (m.find? a).getD b₀
 
@@ -229,10 +226,8 @@ partial def eraseAux [BEq α] : Node α β → USize → α → Node α β × Bo
   | n@(Node.collision keys vals heq), _, k =>
     match keys.indexOf? k with
     | some idx =>
-      let keys' := keys.feraseIdx idx
-      have keq := keys.size_feraseIdx idx
-      let vals' := vals.feraseIdx (Eq.ndrec idx heq)
-      have veq := vals.size_feraseIdx (Eq.ndrec idx heq)
+      let ⟨keys', keq⟩ := keys.eraseIdx' idx
+      let ⟨vals', veq⟩ := vals.eraseIdx' (Eq.ndrec idx heq)
       have : keys.size - 1 = vals.size - 1 := by rw [heq]
       (Node.collision keys' vals' (keq.trans (this.trans veq.symm)), true)
     | none     => (n, false)
@@ -325,9 +320,6 @@ def map {α : Type u} {β : Type v} {σ : Type u} {_ : BEq α} {_ : Hashable α}
 def toList {_ : BEq α} {_ : Hashable α} (m : PersistentHashMap α β) : List (α × β) :=
   m.foldl (init := []) fun ps k v => (k, v) :: ps
 
-def toArray {_ : BEq α} {_ : Hashable α} (m : PersistentHashMap α β) : Array (α × β) :=
-  m.foldl (init := #[]) fun ps k v => ps.push (k, v)
-
 structure Stats where
   numNodes      : Nat := 0
   numNull       : Nat := 0

src/Lean/Data/Position.lean

@@ -38,6 +38,9 @@ structure FileMap where
   The first entry is always `0` and the last always the index of the last character.
   In particular, if the last character is a newline, that index will appear twice. -/
   positions : Array String.Pos
+  /-- The line numbers associated with the `positions`.
+  Has the same length as `positions` and is always of the form `#[1, 2, …, n-1, n-1]`. -/
+  lines     : Array Nat
   deriving Inhabited
 
 class MonadFileMap (m : Type → Type) where
@@ -47,50 +50,40 @@ export MonadFileMap (getFileMap)
 
 namespace FileMap
 
-/-- The last line should always be `positions.size - 1`. -/
-def getLastLine (fmap : FileMap) : Nat :=
-  fmap.positions.size - 1
-
-/-- The line numbers associated with the `positions` of the `FileMap`.
-`fmap.getLine i` is the iᵗʰ entry of `#[1, 2, …, n-1, n-1]`
-where `n` is the `size` of `positions`. -/
-def getLine (fmap : FileMap) (x : Nat) : Nat :=
-  min (x + 1) fmap.getLastLine
-
 partial def ofString (s : String) : FileMap :=
-  let rec loop (i : String.Pos) (line : Nat) (ps : Array String.Pos) : FileMap :=
-    if s.atEnd i then { source := s, positions := ps.push i }
+  let rec loop (i : String.Pos) (line : Nat) (ps : Array String.Pos) (lines : Array Nat) : FileMap :=
+    if s.atEnd i then { source := s, positions := ps.push i, lines := lines.push line }
     else
       let c := s.get i
       let i := s.next i
-      if c == '\n' then loop i (line+1) (ps.push i)
-      else loop i line ps
-  loop 0 1 (#[0])
+      if c == '\n' then loop i (line+1) (ps.push i) (lines.push (line+1))
+      else loop i line ps lines
+  loop 0 1 (#[0]) (#[1])
 
 partial def toPosition (fmap : FileMap) (pos : String.Pos) : Position :=
   match fmap with
-  | { source := str, positions := ps } =>
+  | { source := str, positions := ps, lines := lines } =>
     if ps.size >= 2 && pos <= ps.back then
       let rec toColumn (i : String.Pos) (c : Nat) : Nat :=
         if i == pos || str.atEnd i then c
         else toColumn (str.next i) (c+1)
       let rec loop (b e : Nat) :=
         let posB := ps[b]!
-        if e == b + 1 then { line := fmap.getLine b, column := toColumn posB 0 }
+        if e == b + 1 then { line := lines.get! b, column := toColumn posB 0 }
         else
           let m := (b + e) / 2;
           let posM := ps.get! m;
-          if pos == posM then { line := fmap.getLine m, column := 0 }
+          if pos == posM then { line := lines.get! m, column := 0 }
           else if pos > posM then loop m e
           else loop b m
       loop 0 (ps.size -1)
-    else if ps.isEmpty then
+    else if lines.isEmpty then
       ⟨0, 0⟩
     else
       -- Some systems like the delaborator use synthetic positions without an input file,
       -- which would violate `toPositionAux`'s invariant.
       -- Can also happen with EOF errors, which are not strictly inside the file.
-      ⟨fmap.getLastLine, (pos - ps.back).byteIdx⟩
+      ⟨lines.back, (pos - ps.back).byteIdx⟩
 
 /-- Convert a `Lean.Position` to a `String.Pos`. -/
 def ofPosition (text : FileMap) (pos : Position) : String.Pos :=

src/Lean/Data/Rat.lean

@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.NotationExtra
-import Init.Data.ToString.Macro
+import Init.Data.ToString.Basic
 import Init.Data.Int.DivMod
 import Init.Data.Nat.Gcd
 namespace Lean

src/Lean/Data/Xml/Basic.lean

@@ -5,8 +5,6 @@ Author: Dany Fabian
 -/
 prelude
 import Lean.Data.RBMap
-import Init.Data.ToString.Macro
-
 namespace Lean
 namespace Xml
 

src/Lean/DeclarationRange.lean

@@ -48,14 +48,14 @@ def addDeclarationRanges [MonadEnv m] (declName : Name) (declRanges : Declaratio
 def findDeclarationRangesCore? [Monad m] [MonadEnv m] (declName : Name) : m (Option DeclarationRanges) :=
   return declRangeExt.find? (← getEnv) declName
 
-def findDeclarationRanges? [Monad m] [MonadEnv m] [MonadLiftT BaseIO m] (declName : Name) : m (Option DeclarationRanges) := do
+def findDeclarationRanges? [Monad m] [MonadEnv m] [MonadLiftT IO m] (declName : Name) : m (Option DeclarationRanges) := do
   let env ← getEnv
   let ranges ← if isAuxRecursor env declName || isNoConfusion env declName || (← isRec declName)  then
     findDeclarationRangesCore? declName.getPrefix
   else
     findDeclarationRangesCore? declName
   match ranges with
-  | none => return (← builtinDeclRanges.get (m := BaseIO)).find? declName
+  | none => return (← builtinDeclRanges.get (m := IO)).find? declName
   | some _ => return ranges
 
 end Lean

src/Lean/DocString.lean

@@ -6,7 +6,6 @@ Authors: Leonardo de Moura
 prelude
 import Lean.DeclarationRange
 import Lean.MonadEnv
-import Init.Data.String.Extra
 
 namespace Lean
 
@@ -14,14 +13,12 @@ private builtin_initialize builtinDocStrings : IO.Ref (NameMap String) ← IO.mk
 private builtin_initialize docStringExt : MapDeclarationExtension String ← mkMapDeclarationExtension
 
 def addBuiltinDocString (declName : Name) (docString : String) : IO Unit :=
-  builtinDocStrings.modify (·.insert declName docString.removeLeadingSpaces)
+  builtinDocStrings.modify (·.insert declName (removeLeadingSpaces docString))
 
-def addDocString [Monad m] [MonadError m] [MonadEnv m] (declName : Name) (docString : String) : m Unit := do
-  unless (← getEnv).getModuleIdxFor? declName |>.isNone do
-    throwError s!"invalid doc string, declaration '{declName}' is in an imported module"
-  modifyEnv fun env => docStringExt.insert env declName docString.removeLeadingSpaces
+def addDocString [MonadEnv m] (declName : Name) (docString : String) : m Unit :=
+  modifyEnv fun env => docStringExt.insert env declName (removeLeadingSpaces docString)
 
-def addDocString' [Monad m] [MonadError m] [MonadEnv m] (declName : Name) (docString? : Option String) : m Unit :=
+def addDocString' [Monad m] [MonadEnv m] (declName : Name) (docString? : Option String) : m Unit :=
   match docString? with
   | some docString => addDocString declName docString
   | none => return ()

src/Lean/Elab/App.lean

@@ -1035,7 +1035,7 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
   if eType.isForall then
     match lval with
     | LVal.fieldName _ fieldName _ _ =>
-      let fullName := Name.str `Function fieldName
+      let fullName := `Function ++ fieldName
       if (← getEnv).contains fullName then
         return LValResolution.const `Function `Function fullName
     | _ => pure ()
@@ -1060,9 +1060,9 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
   | some structName, LVal.fieldName _ fieldName _ _ =>
     let env ← getEnv
     let searchEnv : Unit → TermElabM LValResolution := fun _ => do
-      if let some (baseStructName, fullName) := findMethod? env structName (.mkSimple fieldName) then
+      if let some (baseStructName, fullName) := findMethod? env structName fieldName then
         return LValResolution.const baseStructName structName fullName
-      else if let some (structName', fullName) := findMethodAlias? env structName (.mkSimple fieldName) then
+      else if let some (structName', fullName) := findMethodAlias? env structName fieldName then
         return LValResolution.const structName' structName' fullName
       else
         throwLValError e eType
@@ -1149,7 +1149,7 @@ private partial def mkBaseProjections (baseStructName : Name) (structName : Name
 private def typeMatchesBaseName (type : Expr) (baseName : Name) : MetaM Bool := do
   if baseName == `Function then
     return (← whnfR type).isForall
-  else if type.cleanupAnnotations.isAppOf baseName then
+  else if type.consumeMData.isAppOf baseName then
     return true
   else
     return (← whnfR type).isAppOf baseName
@@ -1199,8 +1199,8 @@ private def elabAppLValsAux (namedArgs : Array NamedArg) (args : Array Arg) (exp
   let rec loop : Expr → List LVal → TermElabM Expr
   | f, []          => elabAppArgs f namedArgs args expectedType? explicit ellipsis
   | f, lval::lvals => do
-    if let LVal.fieldName (fullRef := fullRef) .. := lval then
-      addDotCompletionInfo fullRef f expectedType?
+    if let LVal.fieldName (ref := fieldStx) (targetStx := targetStx) .. := lval then
+      addDotCompletionInfo targetStx f expectedType? fieldStx
     let hasArgs := !namedArgs.isEmpty || !args.isEmpty
     let (f, lvalRes) ← resolveLVal f lval hasArgs
     match lvalRes with
@@ -1340,7 +1340,7 @@ private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Arra
     let elabFieldName (e field : Syntax) := do
       let newLVals := field.identComponents.map fun comp =>
         -- We use `none` in `suffix?` since `field` can't be part of a composite name
-        LVal.fieldName comp comp.getId.getString! none f
+        LVal.fieldName comp comp.getId.getString! none e
       elabAppFn e (newLVals ++ lvals) namedArgs args expectedType? explicit ellipsis overloaded acc
     let elabFieldIdx (e idxStx : Syntax) := do
       let some idx := idxStx.isFieldIdx? | throwError "invalid field index"

src/Lean/Elab/BuiltinCommand.lean

@@ -55,7 +55,7 @@ private def popScopes (numScopes : Nat) : CommandElabM Unit :=
 
 private def checkAnonymousScope : List Scope → Option Name
   | { header := "", .. } :: _ => none
-  | { header := h, .. }  :: _ => some <| .mkSimple h
+  | { header := h, .. }  :: _ => some h
   | _                         => some .anonymous -- should not happen
 
 private def checkEndHeader : Name → List Scope → Option Name
@@ -64,7 +64,7 @@ private def checkEndHeader : Name → List Scope → Option Name
     if h == s then
       (.str · s) <$> checkEndHeader p scopes
     else
-      some <| .mkSimple h
+      some h
   | _, _ => some .anonymous -- should not happen
 
 @[builtin_command_elab «namespace»] def elabNamespace : CommandElab := fun stx =>
@@ -536,7 +536,7 @@ def elabCheckCore (ignoreStuckTC : Bool) : CommandElab
     -- show signature for `#check id`/`#check @id`
     if let `($id:ident) := term then
       try
-        for c in (← realizeGlobalConstWithInfos term) do
+        for c in (← resolveGlobalConstWithInfos term) do
           addCompletionInfo <| .id term id.getId (danglingDot := false) {} none
           logInfoAt tk <| .ofPPFormat { pp := fun
             | some ctx => ctx.runMetaM <| PrettyPrinter.ppSignature c
@@ -749,7 +749,7 @@ def elabRunMeta : CommandElab := fun stx =>
     pure ()
 
 @[builtin_command_elab «set_option»] def elabSetOption : CommandElab := fun stx => do
-  let options ← Elab.elabSetOption stx[1] stx[3]
+  let options ← Elab.elabSetOption stx[1] stx[2]
   modify fun s => { s with maxRecDepth := maxRecDepth.get options }
   modifyScope fun scope => { scope with opts := options }
 
@@ -760,7 +760,7 @@ def elabRunMeta : CommandElab := fun stx =>
 @[builtin_command_elab Parser.Command.addDocString] def elabAddDeclDoc : CommandElab := fun stx => do
   match stx with
   | `($doc:docComment add_decl_doc $id) =>
-    let declName ← liftCoreM <| realizeGlobalConstNoOverloadWithInfo id
+    let declName ← resolveGlobalConstNoOverloadWithInfo id
     unless ((← getEnv).getModuleIdxFor? declName).isNone do
       throwError "invalid 'add_decl_doc', declaration is in an imported module"
     if let .none ← findDeclarationRangesCore? declName then

src/Lean/Elab/BuiltinTerm.lean

@@ -223,7 +223,7 @@ def elabScientificLit : TermElab := fun stx expectedType? => do
   | none     => throwIllFormedSyntax
 
 @[builtin_term_elab doubleQuotedName] def elabDoubleQuotedName : TermElab := fun stx _ =>
-  return toExpr (← realizeGlobalConstNoOverloadWithInfo stx[2])
+  return toExpr (← resolveGlobalConstNoOverloadWithInfo stx[2])
 
 @[builtin_term_elab declName] def elabDeclName : TermElab := adaptExpander fun _ => do
   let some declName ← getDeclName?
@@ -232,7 +232,7 @@ def elabScientificLit : TermElab := fun stx expectedType? => do
 
 @[builtin_term_elab Parser.Term.withDeclName] def elabWithDeclName : TermElab := fun stx expectedType? => do
   let id := stx[2].getId
-  let id ← if stx[1].isNone then pure id else pure <| (← getCurrNamespace) ++ id
+  let id := if stx[1].isNone then id else (← getCurrNamespace) ++ id
   let e := stx[3]
   withMacroExpansion stx e <| withDeclName id <| elabTerm e expectedType?
 
@@ -312,9 +312,9 @@ private def mkSilentAnnotationIfHole (e : Expr) : TermElabM Expr := do
     popScope
 
 @[builtin_term_elab «set_option»] def elabSetOption : TermElab := fun stx expectedType? => do
-  let options ← Elab.elabSetOption stx[1] stx[3]
+  let options ← Elab.elabSetOption stx[1] stx[2]
   withTheReader Core.Context (fun ctx => { ctx with maxRecDepth := maxRecDepth.get options, options := options }) do
-    elabTerm stx[5] expectedType?
+    elabTerm stx[4] expectedType?
 
 @[builtin_term_elab withAnnotateTerm] def elabWithAnnotateTerm : TermElab := fun stx expectedType? => do
   match stx with

src/Lean/Elab/Command.lean

@@ -141,8 +141,7 @@ private def addTraceAsMessagesCore (ctx : Context) (log : MessageLog) (traceStat
   let mut log := log
   let traces' := traces.toArray.qsort fun ((a, _), _) ((b, _), _) => a < b
   for ((pos, endPos), traceMsg) in traces' do
-    let data := .tagged `_traceMsg <| .joinSep traceMsg.toList "\n"
-    log := log.add <| mkMessageCore ctx.fileName ctx.fileMap data .information pos endPos
+    log := log.add <| mkMessageCore ctx.fileName ctx.fileMap (.joinSep traceMsg.toList "\n") .information pos endPos
   return log
 
 private def addTraceAsMessages : CommandElabM Unit := do
@@ -269,6 +268,11 @@ instance : MonadRecDepth CommandElabM where
   getRecDepth      := return (← read).currRecDepth
   getMaxRecDepth   := return (← get).maxRecDepth
 
+register_builtin_option showPartialSyntaxErrors : Bool := {
+  defValue := false
+  descr    := "show elaboration errors from partial syntax trees (i.e. after parser recovery)"
+}
+
 builtin_initialize registerTraceClass `Elab.command
 
 partial def elabCommand (stx : Syntax) : CommandElabM Unit := do
@@ -317,6 +321,11 @@ def elabCommandTopLevel (stx : Syntax) : CommandElabM Unit := withRef stx do pro
     -- note the order: first process current messages & info trees, then add back old messages & trees,
     -- then convert new traces to messages
     let mut msgs := (← get).messages
+    -- `stx.hasMissing` should imply `initMsgs.hasErrors`, but the latter should be cheaper to check in general
+    if !showPartialSyntaxErrors.get (← getOptions) && initMsgs.hasErrors && stx.hasMissing then
+      -- discard elaboration errors, except for a few important and unlikely misleading ones, on parse error
+      msgs := ⟨msgs.msgs.filter fun msg =>
+        msg.data.hasTag (fun tag => tag == `Elab.synthPlaceholder || tag == `Tactic.unsolvedGoals || (`_traceMsg).isSuffixOf tag)⟩
     for tree in (← getInfoTrees) do
       trace[Elab.info] (← tree.format)
     modify fun st => { st with
@@ -535,9 +544,9 @@ first evaluates any local `set_option ... in ...` clauses and then invokes `cmd`
 partial def withSetOptionIn (cmd : CommandElab) : CommandElab := fun stx => do
   if stx.getKind == ``Lean.Parser.Command.in &&
      stx[0].getKind == ``Lean.Parser.Command.set_option then
-      let opts ← Elab.elabSetOption stx[0][1] stx[0][3]
+      let opts ← Elab.elabSetOption stx[0][1] stx[0][2]
       Command.withScope (fun scope => { scope with opts }) do
-        withSetOptionIn cmd stx[2]
+        withSetOptionIn cmd stx[1]
   else
     cmd stx
 

src/Lean/Elab/DeclModifiers.lean

@@ -27,8 +27,6 @@ def checkNotAlreadyDeclared {m} [Monad m] [MonadEnv m] [MonadError m] [MonadInfo
     match privateToUserName? declName with
     | none          => throwError "'{declName}' has already been declared"
     | some declName => throwError "private declaration '{declName}' has already been declared"
-  if isReservedName env declName then
-    throwError "'{declName}' is a reserved name"
   if env.contains (mkPrivateName env declName) then
     addInfo (mkPrivateName env declName)
     throwError "a private declaration '{declName}' has already been declared"

src/Lean/Elab/Declaration.lean

@@ -42,7 +42,7 @@ private def isNamedDef (stx : Syntax) : Bool :=
     let decl := stx[1]
     let k := decl.getKind
     k == ``Lean.Parser.Command.abbrev ||
-    k == ``Lean.Parser.Command.definition ||
+    k == ``Lean.Parser.Command.def ||
     k == ``Lean.Parser.Command.theorem ||
     k == ``Lean.Parser.Command.opaque ||
     k == ``Lean.Parser.Command.axiom ||
@@ -95,7 +95,7 @@ private def expandDeclNamespace? (stx : Syntax) : MacroM (Option (Name × Syntax
   let scpView := extractMacroScopes name
   match scpView.name with
   | .str .anonymous _ => return none
-  | .str pre shortName => return some (pre, setDefName stx { scpView with name := .mkSimple shortName }.review)
+  | .str pre shortName => return some (pre, setDefName stx { scpView with name := shortName }.review)
   | _ => return none
 
 def elabAxiom (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
@@ -166,7 +166,7 @@ private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) : Comm
     return { ref := ctor, modifiers := ctorModifiers, declName := ctorName, binders := binders, type? := type? : CtorView }
   let computedFields ← (decl[5].getOptional?.map (·[1].getArgs) |>.getD #[]).mapM fun cf => withRef cf do
     return { ref := cf, modifiers := cf[0], fieldId := cf[1].getId, type := ⟨cf[3]⟩, matchAlts := ⟨cf[4]⟩ }
-  let classes ← liftCoreM <| getOptDerivingClasses decl[6]
+  let classes ← getOptDerivingClasses decl[6]
   return {
     ref             := decl
     shortDeclName   := name
@@ -354,7 +354,7 @@ def elabMutual : CommandElab := fun stx => do
     -/
     let declNames ←
        try
-         realizeGlobalConst ident
+         resolveGlobalConst ident
        catch _ =>
          let name := ident.getId.eraseMacroScopes
          if (← Simp.isBuiltinSimproc name) then

src/Lean/Elab/DefView.lean

@@ -142,7 +142,7 @@ def mkDefViewOfExample (modifiers : Modifiers) (stx : Syntax) : DefView :=
 def isDefLike (stx : Syntax) : Bool :=
   let declKind := stx.getKind
   declKind == ``Parser.Command.abbrev ||
-  declKind == ``Parser.Command.definition ||
+  declKind == ``Parser.Command.def ||
   declKind == ``Parser.Command.theorem ||
   declKind == ``Parser.Command.opaque ||
   declKind == ``Parser.Command.instance ||
@@ -152,7 +152,7 @@ def mkDefView (modifiers : Modifiers) (stx : Syntax) : CommandElabM DefView :=
   let declKind := stx.getKind
   if declKind == ``Parser.Command.«abbrev» then
     return mkDefViewOfAbbrev modifiers stx
-  else if declKind == ``Parser.Command.definition then
+  else if declKind == ``Parser.Command.def then
     return mkDefViewOfDef modifiers stx
   else if declKind == ``Parser.Command.theorem then
     return mkDefViewOfTheorem modifiers stx

src/Lean/Elab/Deriving/Basic.lean

@@ -100,10 +100,10 @@ private def tryApplyDefHandler (className : Name) (declName : Name) : CommandEla
 
 @[builtin_command_elab «deriving»] def elabDeriving : CommandElab
   | `(deriving instance $[$classes $[with $argss?]?],* for $[$declNames],*) => do
-     let declNames ← liftCoreM <| declNames.mapM realizeGlobalConstNoOverloadWithInfo
+     let declNames ← declNames.mapM resolveGlobalConstNoOverloadWithInfo
      for cls in classes, args? in argss? do
        try
-         let className ← liftCoreM <| realizeGlobalConstNoOverloadWithInfo cls
+         let className ← resolveGlobalConstNoOverloadWithInfo cls
          withRef cls do
            if declNames.size == 1 && args?.isNone then
              if (← tryApplyDefHandler className declNames[0]!) then
@@ -118,12 +118,12 @@ structure DerivingClassView where
   className : Name
   args? : Option (TSyntax ``Parser.Term.structInst)
 
-def getOptDerivingClasses (optDeriving : Syntax) : CoreM (Array DerivingClassView) := do
+def getOptDerivingClasses [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadInfoTree m] (optDeriving : Syntax) : m (Array DerivingClassView) := do
   match optDeriving with
   | `(Parser.Command.optDeriving| deriving $[$classes $[with $argss?]?],*) =>
     let mut ret := #[]
     for cls in classes, args? in argss? do
-      let className ← realizeGlobalConstNoOverloadWithInfo cls
+      let className ← resolveGlobalConstNoOverloadWithInfo cls
       ret := ret.push { ref := cls, className := className, args? }
     return ret
   | _ => return #[]

src/Lean/Elab/Deriving/DecEq.lean

@@ -27,9 +27,8 @@ where
       let rhs ← if isProof then
         `(have h : @$a = @$b := rfl; by subst h; exact $(← mkSameCtorRhs todo):term)
       else
-        let sameCtor ← mkSameCtorRhs todo
         `(if h : @$a = @$b then
-           by subst h; exact $sameCtor:term
+           by subst h; exact $(← mkSameCtorRhs todo):term
           else
            isFalse (by intro n; injection n; apply h _; assumption))
       if let some auxFunName := recField then

src/Lean/Elab/Deriving/Ord.lean

@@ -84,7 +84,6 @@ def mkMutualBlock (ctx : Context) : TermElabM Syntax := do
   for i in [:ctx.typeInfos.size] do
     auxDefs := auxDefs.push (← mkAuxFunction ctx i)
   `(mutual
-     set_option match.ignoreUnusedAlts true
      $auxDefs:command*
     end)
 

src/Lean/Elab/Do.lean

@@ -63,9 +63,8 @@ private def letDeclHasBinders (letDecl : Syntax) : Bool :=
 /-- Return true if we should generate an error message when lifting a method over this kind of syntax. -/
 private def liftMethodForbiddenBinder (stx : Syntax) : Bool :=
   let k := stx.getKind
-  -- TODO: make this extensible in the future.
   if k == ``Parser.Term.fun || k == ``Parser.Term.matchAlts ||
-     k == ``Parser.Term.doLetRec || k == ``Parser.Term.letrec then
+     k == ``Parser.Term.doLetRec || k == ``Parser.Term.letrec  then
      -- It is never ok to lift over this kind of binder
     true
   -- The following kinds of `let`-expressions require extra checks to decide whether they contain binders or not
@@ -78,15 +77,12 @@ private def liftMethodForbiddenBinder (stx : Syntax) : Bool :=
   else
     false
 
--- TODO: we must track whether we are inside a quotation or not.
 private partial def hasLiftMethod : Syntax → Bool
   | Syntax.node _ k args =>
     if liftMethodDelimiter k then false
     -- NOTE: We don't check for lifts in quotations here, which doesn't break anything but merely makes this rare case a
     -- bit slower
     else if k == ``Parser.Term.liftMethod then true
-    -- For `pure` if-then-else, we only lift `(<- ...)` occurring in the condition.
-    else if k == ``termDepIfThenElse || k == ``termIfThenElse then args.size >= 2 && hasLiftMethod args[1]!
     else args.any hasLiftMethod
   | _ => false
 
@@ -1325,12 +1321,6 @@ private partial def expandLiftMethodAux (inQuot : Bool) (inBinder : Bool) : Synt
       return .node i k (alts.map (·.1))
     else if liftMethodDelimiter k then
       return stx
-    -- For `pure` if-then-else, we only lift `(<- ...)` occurring in the condition.
-    else if args.size >= 2 && (k == ``termDepIfThenElse || k == ``termIfThenElse) then do
-      let inAntiquot := stx.isAntiquot && !stx.isEscapedAntiquot
-      let arg1 ← expandLiftMethodAux (inQuot && !inAntiquot || stx.isQuot) inBinder args[1]!
-      let args := args.set! 1 arg1
-      return Syntax.node i k args
     else if k == ``Parser.Term.liftMethod && !inQuot then withFreshMacroScope do
       if inBinder then
         throwErrorAt stx "cannot lift `(<- ...)` over a binder, this error usually happens when you are trying to lift a method nested in a `fun`, `let`, or `match`-alternative, and it can often be fixed by adding a missing `do`"