doc-string

This PR refactors the `NoNatZeroDivisors` to make sure it will work
with the new `Semiring` support.

.github/actionlint.yaml

@@ -1,5 +0,0 @@
-self-hosted-runner:
-  labels:
-    - nscloud-ubuntu-22.04-amd64-4x16
-    - nscloud-ubuntu-22.04-amd64-8x16
-    - nscloud-macos-sonoma-arm64-6x14

.github/workflows/awaiting-manual.yml

@@ -1,38 +0,0 @@
-name: Check awaiting-manual label
-
-on:
-  merge_group:
-  pull_request:
-    types: [opened, synchronize, reopened, labeled, unlabeled]
-
-jobs:
-  check-awaiting-manual:
-    runs-on: ubuntu-latest
-    steps:
-      - name: Check awaiting-manual label
-        id: check-awaiting-manual-label
-        if: github.event_name == 'pull_request'
-        uses: actions/github-script@v7
-        with:
-          script: |
-            const { labels, number: prNumber } = context.payload.pull_request;
-            const hasAwaiting = labels.some(label => label.name == "awaiting-manual");
-            const hasBreaks = labels.some(label => label.name == "breaks-manual");
-            const hasBuilds = labels.some(label => label.name == "builds-manual");
-
-            if (hasAwaiting && hasBreaks) {
-              core.setFailed('PR has both "awaiting-manual" and "breaks-manual" labels.');
-            } else if (hasAwaiting && !hasBreaks && !hasBuilds) {
-              core.info('PR is marked "awaiting-manual" but neither "breaks-manual" nor "builds-manual" labels are present.');
-              core.setOutput('awaiting', 'true');
-            }
-      
-      - name: Wait for manual compatibility
-        if: github.event_name == 'pull_request' && steps.check-awaiting-manual-label.outputs.awaiting == 'true'
-        run: |
-          echo "::notice title=Awaiting manual::PR is marked 'awaiting-manual' but neither 'breaks-manual' nor 'builds-manual' labels are present."
-          echo "This check will remain in progress until the PR is updated with appropriate manual compatibility labels."
-          # Keep the job running indefinitely to show "in progress" status
-          while true; do
-            sleep 3600  # Sleep for 1 hour at a time
-          done

.github/workflows/build-template.yml

@@ -97,17 +97,16 @@ jobs:
           sudo apt-get update
           sudo apt-get install -y gcc-multilib g++-multilib ccache libuv1-dev:i386 pkgconf:i386
         if: matrix.cmultilib
-      - name: Restore Cache
+      - name: Cache
         id: restore-cache
         uses: actions/cache/restore@v4
         with:
-          # NOTE: must be in sync with `save` below and with `restore-cache` in `update-stage0.yml`
+          # NOTE: must be in sync with `save` below
           path: |
             .ccache
-            ${{ matrix.name == 'Linux Lake (cached)' && 'build/stage1/**/*.trace
+            ${{ matrix.name == 'Linux Lake' && false && 'build/stage1/**/*.trace
             build/stage1/**/*.olean*
             build/stage1/**/*.ilean
-            build/stage1/**/*.ir
             build/stage1/**/*.c
             build/stage1/**/*.c.o*' || '' }}
           key: ${{ matrix.name }}-build-v3-${{ github.sha }}
@@ -119,15 +118,9 @@ jobs:
         run: |
           ccache --zero-stats
         if: runner.os == 'Linux'
-      - name: Set up env
+      - name: Set up NPROC
         run: |
           echo "NPROC=$(nproc 2>/dev/null || sysctl -n hw.logicalcpu 2>/dev/null || echo 4)" >> $GITHUB_ENV
-          if ! diff src/stdlib_flags.h stage0/src/stdlib_flags.h; then
-            echo "src/stdlib_flags.h and stage0/src/stdlib_flags.h differ, will test and pack stage 2"
-            echo "TARGET_STAGE=stage2" >> $GITHUB_ENV
-          else
-            echo "TARGET_STAGE=stage1" >> $GITHUB_ENV
-          fi
       - name: Build
         run: |
           ulimit -c unlimited  # coredumps
@@ -148,9 +141,6 @@ jobs:
           if [[ -n '${{ matrix.prepare-llvm }}' ]]; then
             wget -q ${{ matrix.llvm-url }}
             PREPARE="$(${{ matrix.prepare-llvm }})"
-            if [ "$TARGET_STAGE" == "stage2" ]; then
-              cp -r stage1 stage2
-            fi
             eval "OPTIONS+=($PREPARE)"
           fi
           if [[ -n '${{ matrix.release }}' && -n '${{ inputs.nightly }}' ]]; then
@@ -165,10 +155,10 @@ jobs:
           fi
           # contortion to support empty OPTIONS with old macOS bash
           cmake .. --preset ${{ matrix.CMAKE_PRESET || 'release' }} -B . ${{ matrix.CMAKE_OPTIONS }} ${OPTIONS[@]+"${OPTIONS[@]}"} -DLEAN_INSTALL_PREFIX=$PWD/..
-          time make $TARGET_STAGE -j$NPROC
+          time make -j$NPROC
       - name: Install
         run: |
-          make -C build/$TARGET_STAGE install
+          make -C build install
       - name: Check Binaries
         run: ${{ matrix.binary-check }} lean-*/bin/* || true
       - name: Count binary symbols
@@ -199,18 +189,18 @@ jobs:
           path: pack/*
       - name: Lean stats
         run: |
-          build/stage1/bin/lean --stats src/Lean.lean -Dexperimental.module=true
+          build/stage1/bin/lean --stats src/Lean.lean
         if: ${{ !matrix.cross }}
       - name: Test
         id: test
         run: |
           ulimit -c unlimited  # coredumps
-          time ctest --preset ${{ matrix.CMAKE_PRESET || 'release' }} --test-dir build/$TARGET_STAGE -j$NPROC --output-junit test-results.xml
+          time ctest --preset ${{ matrix.CMAKE_PRESET || 'release' }} --test-dir build/stage1 -j$NPROC --output-junit test-results.xml ${{ matrix.CTEST_OPTIONS }}
         if: (matrix.wasm || !matrix.cross) && (inputs.check-level >= 1 || matrix.test)
       - name: Test Summary
         uses: test-summary/action@v2
         with:
-          paths: build/${{ env.TARGET_STAGE }}/test-results.xml
+          paths: build/stage1/test-results.xml
         # prefix `if` above with `always` so it's run even if tests failed
         if: always() && steps.test.conclusion != 'skipped'
       - name: Check Test Binary
@@ -235,13 +225,8 @@ jobs:
         if: matrix.test-speedcenter
       - name: Check rebootstrap
         run: |
-          set -e
-          # clean rebuild in case of Makefile changes/Lake does not detect uncommited stage 0
-          # changes yet
-          make -C build update-stage0
-          make -C build/stage1 clean-stdlib
-          time make -C build -j$NPROC
-          time ctest --preset ${{ matrix.CMAKE_PRESET || 'release' }} --test-dir build/stage1 -j$NPROC
+          # clean rebuild in case of Makefile changes
+          make -C build update-stage0 && rm -rf build/stage* && make -C build -j$NPROC
         if: matrix.check-rebootstrap
       - name: CCache stats
         if: always()
@@ -260,15 +245,9 @@ jobs:
           # NOTE: must be in sync with `restore` above
           path: |
             .ccache
-            ${{ matrix.name == 'Linux Lake (cached)' && 'build/stage1/**/*.trace
+            ${{ matrix.name == 'Linux Lake' && false && 'build/stage1/**/*.trace
             build/stage1/**/*.olean*
             build/stage1/**/*.ilean
-            build/stage1/**/*.ir
             build/stage1/**/*.c
             build/stage1/**/*.c.o*' || '' }}
           key: ${{ steps.restore-cache.outputs.cache-primary-key }}
-      - name: Upload Build Artifact
-        if: always() && matrix.name == 'Linux Lake (cached)'
-        uses: actions/upload-artifact@v4
-        with:
-          path: build

.github/workflows/ci.yml

@@ -145,7 +145,6 @@ jobs:
             // use large runners where available (original repo)
             let large = ${{ github.repository == 'leanprover/lean4' }};
             const isPr = "${{ github.event_name }}" == "pull_request";
-            const isPushToMaster = "${{ github.event_name }}" == "push" && "${{ github.ref_name }}" == "master";
             let matrix = [
               /* TODO: to be updated to new LLVM
               {
@@ -165,16 +164,14 @@ jobs:
               {
                 // portable release build: use channel with older glibc (2.26)
                 "name": "Linux release",
-                "os": "ubuntu-latest",
+                "os": large && level < 2 ? "nscloud-ubuntu-22.04-amd64-4x16" : "ubuntu-latest",
                 "release": true,
                 // Special handling for release jobs. We want:
-                // 1. To run it in PRs so developers get PR toolchains (so secondary is sufficient)
+                // 1. To run it in PRs so developrs get PR toolchains (so secondary is sufficient)
                 // 2. To skip it in merge queues as it takes longer than the
                 //    Linux lake build and adds little value in the merge queue
                 // 3. To run it in release (obviously)
-                // 4. To run it for pushes to master so that pushes to master have a Linux toolchain
-                //    available as an artifact for Grove to use.
-                "check-level": (isPr || isPushToMaster) ? 0 : 2,
+                "check-level": isPr ? 0 : 2,
                 "secondary": isPr,
                 "shell": "nix develop .#oldGlibc -c bash -euxo pipefail {0}",
                 "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-linux-gnu.tar.zst",
@@ -194,13 +191,6 @@ jobs:
                 "test-speedcenter": large && level >= 2,
                 "CMAKE_OPTIONS": "-DUSE_LAKE=ON",
               },
-              {
-                "name": "Linux Lake (cached)",
-                "os": "ubuntu-latest",
-                "check-level": (isPr || isPushToMaster) ? 0 : 2,
-                "secondary": true,
-                "CMAKE_OPTIONS": "-DUSE_LAKE=ON",
-              },
               {
                 "name": "Linux Reldebug",
                 "os": "ubuntu-latest",
@@ -232,8 +222,8 @@ jobs:
               },
               {
                 "name": "macOS aarch64",
-                // standard GH runner only comes with 7GB so use large runner if possible when running tests
-                "os": large && !isPr ? "nscloud-macos-sonoma-arm64-6x14" : "macos-14",
+                // standard GH runner only comes with 7GB so use large runner if possible
+                "os": large ? "nscloud-macos-sonoma-arm64-6x14" : "macos-14",
                 "CMAKE_OPTIONS": "-DLEAN_INSTALL_SUFFIX=-darwin_aarch64",
                 "release": true,
                 "shell": "bash -euxo pipefail {0}",
@@ -241,13 +231,13 @@ jobs:
                 "prepare-llvm": "../script/prepare-llvm-macos.sh lean-llvm*",
                 "binary-check": "otool -L",
                 "tar": "gtar", // https://github.com/actions/runner-images/issues/2619
-                // See "Linux release" for release job levels; Grove is not a concern here
+                // See above for release job levels
                 "check-level": isPr ? 0 : 2,
                 "secondary": isPr,
               },
               {
                 "name": "Windows",
-                "os": large && level == 2 ? "namespace-profile-windows-amd64-4x16" : "windows-2022",
+                "os": "windows-2022",
                 "release": true,
                 "check-level": 2,
                 "shell": "msys2 {0}",
@@ -370,7 +360,7 @@ jobs:
         with:
           path: artifacts
       - name: Release
-        uses: softprops/action-gh-release@72f2c25fcb47643c292f7107632f7a47c1df5cd8
+        uses: softprops/action-gh-release@da05d552573ad5aba039eaac05058a918a7bf631
         with:
           files: artifacts/*/*
           fail_on_unmatched_files: true
@@ -414,7 +404,7 @@ jobs:
           echo -e "\n*Full commit log*\n" >> diff.md
           git log --oneline "$last_tag"..HEAD | sed 's/^/* /' >> diff.md
       - name: Release Nightly
-        uses: softprops/action-gh-release@72f2c25fcb47643c292f7107632f7a47c1df5cd8
+        uses: softprops/action-gh-release@da05d552573ad5aba039eaac05058a918a7bf631
         with:
           body_path: diff.md
           prerelease: true
@@ -431,6 +421,6 @@ jobs:
           GITHUB_TOKEN: ${{ secrets.RELEASE_INDEX_TOKEN }}
       - name: Update toolchain on mathlib4's nightly-testing branch
         run: |
-          gh workflow -R leanprover-community/mathlib4-nightly-testing run nightly_bump_toolchain.yml
+          gh workflow -R leanprover-community/mathlib4 run nightly_bump_toolchain.yml
         env:
           GITHUB_TOKEN: ${{ secrets.MATHLIB4_BOT }}

.github/workflows/grove.yml

@@ -1,161 +0,0 @@
-name: Grove
-
-on:
-  workflow_run: # https://docs.github.com/en/actions/using-workflows/events-that-trigger-workflows#workflow_run
-    workflows: [CI]
-    types: [completed]
-
-permissions:
-  pull-requests: write
-
-jobs:
-  grove-build:
-    runs-on: ubuntu-latest
-    if: github.event.workflow_run.conclusion == 'success' && github.repository == 'leanprover/lean4'
-
-    steps:
-      - name: Retrieve information about the original workflow
-        uses: potiuk/get-workflow-origin@v1_1 # https://github.com/marketplace/actions/get-workflow-origin
-        # This action is deprecated and archived, but it seems hard to find a
-        # better solution for getting the PR number
-        # see https://github.com/orgs/community/discussions/25220 for some discussion
-        id: workflow-info
-        with:
-          token: ${{ secrets.GITHUB_TOKEN }}
-          sourceRunId: ${{ github.event.workflow_run.id }}
-
-      - name: Check if should run
-        id: should-run
-        run: |
-          # Check if it's a push to master (no PR number and target branch is master)
-          if [ -z "${{ steps.workflow-info.outputs.pullRequestNumber }}" ]; then
-            if [ "${{ github.event.workflow_run.head_branch }}" = "master" ]; then
-              echo "Push to master detected. Running Grove."
-              echo "should-run=true" >> "$GITHUB_OUTPUT"
-            else
-              echo "Push to non-master branch, skipping"
-              echo "should-run=false" >> "$GITHUB_OUTPUT"
-            fi
-          else
-            # Check if it's a PR with grove label
-            PR_LABELS='${{ steps.workflow-info.outputs.pullRequestLabels }}'
-            if echo "$PR_LABELS" | grep -q '"grove"'; then
-              echo "PR with grove label detected. Running Grove."
-              echo "should-run=true" >> "$GITHUB_OUTPUT"
-            else
-              echo "PR without grove label, skipping"
-              echo "should-run=false" >> "$GITHUB_OUTPUT"
-            fi
-          fi
-
-      - name: Fetch upstream invalidated facts
-        if: ${{ steps.should-run.outputs.should-run == 'true' && steps.workflow-info.outputs.pullRequestNumber != '' }}
-        id: fetch-upstream
-        uses: TwoFx/grove-action/fetch-upstream@v0.4
-        with:
-          artifact-name: grove-invalidated-facts
-          base-ref: master
-
-      - name: Download toolchain for this commit
-        if: ${{ steps.should-run.outputs.should-run == 'true' }}
-        id: download-toolchain
-        uses: dawidd6/action-download-artifact@v11
-        with:
-          commit: ${{ steps.workflow-info.outputs.sourceHeadSha }}
-          workflow: ci.yml
-          path: artifacts
-          name: "build-Linux release"
-          name_is_regexp: true
-
-      - name: Unpack toolchain
-        if: ${{ steps.should-run.outputs.should-run == 'true' }}
-        id: unpack-toolchain
-        run: |
-          cd artifacts
-          # Find the tar.zst file
-          TAR_FILE=$(find . -name "lean-*.tar.zst" -type f | head -1)
-          if [ -z "$TAR_FILE" ]; then
-            echo "Error: No lean-*.tar.zst file found"
-            exit 1
-          fi
-          echo "Found archive: $TAR_FILE"
-
-          # Extract the archive
-          tar --zstd -xf "$TAR_FILE"
-
-          # Find the extracted directory name
-          LEAN_DIR=$(find . -maxdepth 1 -name "lean-*" -type d | head -1)
-          if [ -z "$LEAN_DIR" ]; then
-            echo "Error: No lean-* directory found after extraction"
-            exit 1
-          fi
-          echo "Extracted directory: $LEAN_DIR"
-          echo "lean-dir=$LEAN_DIR" >> "$GITHUB_OUTPUT"
-
-      - name: Build
-        if: ${{ steps.should-run.outputs.should-run == 'true' }}
-        id: build
-        uses: TwoFx/grove-action/build@v0.4
-        with:
-          project-path: doc/std/grove
-          script-name: grove-stdlib
-          invalidated-facts-artifact-name: grove-invalidated-facts
-          comment-artifact-name: grove-comment
-          toolchain-id: lean4
-          toolchain-path: artifacts/${{ steps.unpack-toolchain.outputs.lean-dir }}
-          project-ref: ${{ steps.workflow-info.outputs.sourceHeadSha }}
-
-      # deploy-alias computes a URL component for the PR preview. This
-      # is so we can have a stable name to use for feedback on draft
-      # material.
-      - id: deploy-alias
-        if: ${{ steps.should-run.outputs.should-run == 'true' }}
-        uses: actions/github-script@v7
-        name: Compute Alias
-        with:
-          result-encoding: string
-          script: |
-            if (process.env.PR) {
-                return `pr-${process.env.PR}`
-            } else {
-                return 'deploy-preview-main';
-            }
-        env:
-          PR: ${{ steps.workflow-info.outputs.pullRequestNumber }}
-
-      - name: Deploy to Netlify
-        if: ${{ steps.should-run.outputs.should-run == 'true' }}
-        id: deploy-draft
-        uses: nwtgck/actions-netlify@v3.0
-        with:
-          publish-dir: ${{ steps.build.outputs.out-path }}
-          production-deploy: false
-          github-token: ${{ secrets.GITHUB_TOKEN }}
-          alias: ${{ steps.deploy-alias.outputs.result }}
-          enable-commit-comment: false
-          enable-pull-request-comment: false
-          fails-without-credentials: true
-          enable-github-deployment: false
-          enable-commit-status: false
-        env:
-          NETLIFY_AUTH_TOKEN: ${{ secrets.NETLIFY_AUTH_TOKEN }}
-          NETLIFY_SITE_ID: "1cacfa39-a11c-467c-99e7-2e01d7b4089e"
-
-      # actions-netlify cannot add deploy links to a PR because it assumes a
-      # pull_request context, not a workflow_run context, see
-      # https://github.com/nwtgck/actions-netlify/issues/545
-      # We work around by using a comment to post the latest link
-      - name: "Comment on PR with preview links"
-        uses: marocchino/sticky-pull-request-comment@v2
-        if: ${{ steps.should-run.outputs.should-run == 'true' && steps.workflow-info.outputs.pullRequestNumber != '' }}
-        with:
-          number: ${{ env.PR_NUMBER }}
-          header: preview-comment
-          recreate: true
-          message: |
-            [Grove](${{ steps.deploy-draft.outputs.deploy-url }}) for revision ${{ steps.workflow-info.outputs.sourceHeadSha }}.
-
-            ${{ steps.build.outputs.comment-text }}
-        env:
-          PR_NUMBER: ${{ steps.workflow-info.outputs.pullRequestNumber }}
-          PR_HEADSHA: ${{ steps.workflow-info.outputs.sourceHeadSha }}

.github/workflows/pr-release.yml

@@ -34,7 +34,7 @@ jobs:
       - name: Download artifact from the previous workflow.
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
         id: download-artifact
-        uses: dawidd6/action-download-artifact@v11 # https://github.com/marketplace/actions/download-workflow-artifact
+        uses: dawidd6/action-download-artifact@v10 # https://github.com/marketplace/actions/download-workflow-artifact
         with:
           run_id: ${{ github.event.workflow_run.id }}
           path: artifacts
@@ -71,7 +71,7 @@ jobs:
           GH_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }}
       - name: Release (short format)
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        uses: softprops/action-gh-release@72f2c25fcb47643c292f7107632f7a47c1df5cd8
+        uses: softprops/action-gh-release@da05d552573ad5aba039eaac05058a918a7bf631
         with:
           name: Release for PR ${{ steps.workflow-info.outputs.pullRequestNumber }}
           # There are coredumps files here as well, but all in deeper subdirectories.
@@ -86,7 +86,7 @@ jobs:
 
       - name: Release (SHA-suffixed format)
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        uses: softprops/action-gh-release@72f2c25fcb47643c292f7107632f7a47c1df5cd8
+        uses: softprops/action-gh-release@da05d552573ad5aba039eaac05058a918a7bf631
         with:
           name: Release for PR ${{ steps.workflow-info.outputs.pullRequestNumber }} (${{ steps.workflow-info.outputs.sourceHeadSha }})
           # There are coredumps files here as well, but all in deeper subdirectories.
@@ -151,10 +151,10 @@ jobs:
 
       - name: 'Setup jq'
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        uses: dcarbone/install-jq-action@v3.2.0
+        uses: dcarbone/install-jq-action@v3.1.1
 
       # Check that the most recently nightly coincides with 'git merge-base HEAD master'
-      - name: Check merge-base and nightly-testing-YYYY-MM-DD for Mathlib/Batteries
+      - name: Check merge-base and nightly-testing-YYYY-MM-DD
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
         id: ready
         run: |
@@ -167,7 +167,7 @@ jobs:
             echo "The merge base of this PR coincides with the nightly release"
 
             BATTERIES_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover-community/batteries.git nightly-testing-"$MOST_RECENT_NIGHTLY")"
-            MATHLIB_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover-community/mathlib4-nightly-testing.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 "$BATTERIES_REMOTE_TAGS" ]]; then
               echo "... and Batteries has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
@@ -183,6 +183,7 @@ jobs:
               echo "... but Batteries does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
               MESSAGE="- ❗ Batteries 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\`, Batteries CI should run now."
             fi
+
           else
             echo "The most recently nightly tag on this branch has SHA: $NIGHTLY_SHA"
             echo "but 'git merge-base origin/master HEAD' reported: $MERGE_BASE_SHA"
@@ -264,108 +265,6 @@ jobs:
             echo "mathlib_ready=true" >> "$GITHUB_OUTPUT"
           fi
 
-      - name: Check merge-base and nightly-testing-YYYY-MM-DD for reference manual
-        if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        id: reference-manual-ready
-        run: |
-          echo "Most recent nightly release in your branch: $MOST_RECENT_NIGHTLY"
-          NIGHTLY_SHA=$(git -C lean4.git rev-parse "nightly-$MOST_RECENT_NIGHTLY^{commit}")
-          echo "SHA of most recent nightly release: $NIGHTLY_SHA"
-          MERGE_BASE_SHA=$(git -C lean4.git merge-base origin/master "${{ steps.workflow-info.outputs.sourceHeadSha }}")
-          echo "SHA of merge-base: $MERGE_BASE_SHA"
-          if [ "$NIGHTLY_SHA" = "$MERGE_BASE_SHA" ]; then
-            echo "The merge base of this PR coincides with the nightly release"
-
-            MANUAL_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover/reference-manual.git nightly-testing-"$MOST_RECENT_NIGHTLY")"
-            if [[ -n "$MANUAL_REMOTE_TAGS" ]]; then
-              echo "... and the reference manual has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
-              MESSAGE=""
-            else
-              echo "... but the reference manual does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
-              MESSAGE="- ❗ Reference manual 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-manual\`, reference manual CI should run now."
-            fi
-          else
-            echo "The most recently nightly tag on this branch has SHA: $NIGHTLY_SHA"
-            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-manual
-            NIGHTLY_WITH_MANUAL_SHA="$(git -C lean4.git rev-parse "origin/nightly-with-manual")"
-            MESSAGE="- ❗ Reference manual CI will not be attempted unless your PR branches off the \`nightly-with-manual\` branch. Try \`git rebase $MERGE_BASE_SHA --onto $NIGHTLY_WITH_MANUAL_SHA\`."
-          fi
-
-          if [[ -n "$MESSAGE" ]]; then
-            # Check if force-manual-ci label is present
-            LABELS="$(curl --retry 3 --location --silent \
-                          -H "Authorization: token ${{ secrets.MANUAL_COMMENT_BOT }}" \
-                          -H "Accept: application/vnd.github.v3+json" \
-                          "https://api.github.com/repos/leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/labels" \
-                          | jq -r '.[].name')"
-            
-            if echo "$LABELS" | grep -q "^force-manual-ci$"; then
-              echo "force-manual-ci label detected, forcing CI despite issues"
-              MESSAGE="Forcing reference manual CI because the \`force-manual-ci\` label is present, despite problem: $MESSAGE"
-              FORCE_CI=true
-            else
-              MESSAGE="$MESSAGE You can force reference manual CI using the \`force-manual-ci\` label."
-            fi
-
-            echo "Checking existing messages"
-
-            # The code for updating comments is duplicated in the reference manual's
-            # scripts/lean-pr-testing-comments.sh
-            # so keep in sync
-
-            # Use GitHub API to check if a comment already exists
-            existing_comment="$(curl --retry 3 --location --silent \
-                                    -H "Authorization: token ${{ secrets.MANUAL_COMMENT_BOT }}" \
-                                    -H "Accept: application/vnd.github.v3+json" \
-                                    "https://api.github.com/repos/leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/comments" \
-                                    | jq 'first(.[] | select(.body | test("^- . Manual") or startswith("Reference manual CI status")) | select(.user.login == "leanprover-bot"))')"
-            existing_comment_id="$(echo "$existing_comment" | jq -r .id)"
-            existing_comment_body="$(echo "$existing_comment" | jq -r .body)"
-
-            if [[ "$existing_comment_body" != *"$MESSAGE"* ]]; then
-              MESSAGE="$MESSAGE ($(date "+%Y-%m-%d %H:%M:%S"))"
-
-              echo "Posting message to the comments: $MESSAGE"
-
-              # Append new result to the existing comment or post a new comment
-              # It's essential we use the MANUAL_COMMENT_BOT token here, so that reference manual CI can subsequently edit the comment.
-              if [ -z "$existing_comment_id" ]; then
-                INTRO="Reference manual CI status:"
-                # Post new comment with a bullet point
-                echo "Posting as new comment at leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/comments"
-                curl -L -s \
-                  -X POST \
-                  -H "Authorization: token ${{ secrets.MANUAL_COMMENT_BOT }}" \
-                  -H "Accept: application/vnd.github.v3+json" \
-                  -d "$(jq --null-input --arg intro "$INTRO" --arg val "$MESSAGE" '{"body":($intro + "\n" + $val)}')" \
-                  "https://api.github.com/repos/leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/comments"
-              else
-                # Append new result to the existing comment
-                echo "Appending to existing comment at leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/comments"
-                curl -L -s \
-                  -X PATCH \
-                  -H "Authorization: token ${{ secrets.MANUAL_COMMENT_BOT }}" \
-                  -H "Accept: application/vnd.github.v3+json" \
-                  -d "$(jq --null-input --arg existing "$existing_comment_body" --arg message "$MESSAGE" '{"body":($existing + "\n" + $message)}')" \
-                  "https://api.github.com/repos/leanprover/lean4/issues/comments/$existing_comment_id"
-              fi
-            else
-              echo "The message already exists in the comment body."
-            fi
-
-            if [[ "$FORCE_CI" == "true" ]]; then
-              echo "manual_ready=true" >> "$GITHUB_OUTPUT"
-            else
-              echo "manual_ready=false" >> "$GITHUB_OUTPUT"
-            fi
-          else
-            echo "manual_ready=true" >> "$GITHUB_OUTPUT"
-          fi
-
-
       - name: Report mathlib base
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true' }}
         uses: actions/github-script@v7
@@ -456,7 +355,7 @@ jobs:
         if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
         uses: actions/checkout@v4
         with:
-          repository: leanprover-community/mathlib4-nightly-testing
+          repository: leanprover-community/mathlib4
           token: ${{ secrets.MATHLIB4_BOT }}
           ref: nightly-testing
           fetch-depth: 0 # This ensures we check out all tags and branches.
@@ -512,63 +411,3 @@ jobs:
         if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
         run: |
           git push origin lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}
-
-      # We next automatically create a reference manual branch using this toolchain.
-      # Reference manual CI will be responsible for reporting back success or failure
-      # to the PR comments asynchronously (and thus transitively SubVerso/Verso).
-      - name: Cleanup workspace
-        if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.reference-manual-ready.outputs.manual_ready == 'true'
-        run: |
-          sudo rm -rf ./*
-
-      # Checkout the reference manual repository with all branches
-      - name: Checkout mathlib4 repository
-        if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.reference-manual-ready.outputs.manual_ready == 'true'
-        uses: actions/checkout@v4
-        with:
-          repository: leanprover/reference-manual
-          token: ${{ secrets.MANUAL_PR_BOT }}
-          ref: nightly-testing
-          fetch-depth: 0 # This ensures we check out all tags and branches.
-
-      - name: Check if tag in reference manual exists
-        if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.reference-manual-ready.outputs.manual_ready == 'true'
-        id: check_manual_tag
-        run: |
-          git config user.name "leanprover-bot"
-          git config user.email "leanprover-bot@lean-fro.org"
-
-          if git ls-remote --heads --tags --exit-code origin "nightly-testing-${MOST_RECENT_NIGHTLY}" >/dev/null; then
-            BASE="nightly-testing-${MOST_RECENT_NIGHTLY}"
-          else
-            echo "Couldn't find a 'nightly-testing-${MOST_RECENT_NIGHTLY}' branch in the reference manual. Falling back to 'nightly-testing'."
-            BASE=nightly-testing
-          fi
-
-          echo "Using base tag: $BASE"
-
-          EXISTS="$(git ls-remote --heads origin lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} | wc -l)"
-          echo "Branch exists: $EXISTS"
-          if [ "$EXISTS" = "0" ]; then
-            echo "Branch does not exist, creating it."
-            git switch -c lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} "$BASE"
-            echo "leanprover/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }}" > lean-toolchain
-            git add lean-toolchain
-            git add lakefile.lean lake-manifest.json
-            git commit -m "Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
-          else
-            echo "Branch already exists, updating lean-toolchain."
-            git switch lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}
-            # The reference manual's `nightly-testing` branch or `nightly-testing-YYYY-MM-DD` tag may have moved since this branch was created, so merge their changes.
-            # (This should no longer be possible once `nightly-testing-YYYY-MM-DD` is a tag, but it is still safe to merge.)
-            git merge "$BASE" --strategy-option ours --no-commit --allow-unrelated-histories
-            echo "leanprover/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }}" > lean-toolchain
-            git add lean-toolchain
-            git add lake-manifest.json
-            git commit -m "Update lean-toolchain for https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
-          fi
-
-      - name: Push changes
-        if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.reference-manual-ready.outputs.manual_ready == 'true'
-        run: |
-          git push origin lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}

.github/workflows/update-stage0.yml

@@ -18,7 +18,7 @@ concurrency:
 
 jobs:
   update-stage0:
-    runs-on: nscloud-ubuntu-22.04-amd64-8x16
+    runs-on: ubuntu-latest
     steps:
     # This action should push to an otherwise protected branch, so it
     # uses a deploy key with write permissions, as suggested at
@@ -52,18 +52,6 @@ jobs:
       run: |
         echo "NPROC=$(nproc 2>/dev/null || sysctl -n hw.logicalcpu 2>/dev/null || echo 4)" >> $GITHUB_ENV
       shell: 'nix develop -c bash -euxo pipefail {0}'
-    - name: Restore Cache
-      if: env.should_update_stage0 == 'yes'
-      uses: actions/cache/restore@v4
-      with:
-        # NOTE: must be in sync with `restore-cache` in `build-template.yml`
-        # TODO: actually switch to USE_LAKE once it caches more; for now it just caches more often than any other build type so let's use its cache
-        path: |
-          .ccache
-        key: Linux Lake-build-v3-${{ github.sha }}
-        # fall back to (latest) previous cache
-        restore-keys: |
-          Linux Lake-build-v3
     - if: env.should_update_stage0 == 'yes'
       run: cmake --preset release
       shell: 'nix develop -c bash -euxo pipefail {0}'

.gitignore

@@ -31,4 +31,3 @@ fwOut.txt
 wdErr.txt
 wdIn.txt
 wdOut.txt
-downstream_releases/

CMakeLists.txt

@@ -16,7 +16,7 @@ foreach(var ${vars})
     list(APPEND STAGE1_ARGS "-D${CMAKE_MATCH_1}=${${var}}")
   elseif("${currentHelpString}" MATCHES "No help, variable specified on the command line." OR "${currentHelpString}" STREQUAL "")
     list(APPEND CL_ARGS "-D${var}=${${var}}")
-    if("${var}" MATCHES "USE_GMP|CHECK_OLEAN_VERSION|LEAN_VERSION_.*|LEAN_SPECIAL_VERSION_DESC")
+    if("${var}" MATCHES "USE_GMP|CHECK_OLEAN_VERSION")
       # must forward options that generate incompatible .olean format
       list(APPEND STAGE0_ARGS "-D${var}=${${var}}")
     elseif("${var}" MATCHES "LLVM*|PKG_CONFIG|USE_LAKE|USE_MIMALLOC")

CODEOWNERS

@@ -45,10 +45,3 @@
 /src/Std/Tactic/BVDecide/ @hargoniX
 /src/Lean/Elab/Tactic/BVDecide/ @hargoniX
 /src/Std/Sat/ @hargoniX
-/src/Std/Do @sgraf812
-/src/Std/Tactic/Do @sgraf812
-/src/Lean/Elab/Tactic/Do @sgraf812
-/src/Init/Data/Range/Polymorphic @datokrat
-/src/Init/Data/Slice @datokrat
-/src/Init/Data/Iterators @datokrat
-/src/Std/Data/Iterators @datokrat

doc/dev/ffi.md

@@ -68,7 +68,7 @@ The memory order of the fields is derived from the types and order of the fields
 * Fields of type `USize`
 * Other scalar fields, in decreasing order by size
 
-Within each group the fields are ordered in declaration order. Trivial wrapper types count as their underlying wrapped type for this purpose.
+Within each group the fields are ordered in declaration order. **Warning**: Trivial wrapper types still count toward a field being treated as non-scalar for this purpose.
 
 * To access fields of the first kind, use `lean_ctor_get(val, i)` to get the `i`th non-scalar field.
 * To access `USize` fields, use `lean_ctor_get_usize(val, n+i)` to get the `i`th usize field and `n` is the total number of fields of the first kind.
@@ -80,32 +80,32 @@ structure S where
   ptr_1 : Array Nat
   usize_1 : USize
   sc64_1 : UInt64
-  sc64_2 : { x : UInt64 // x > 0 } -- wrappers of scalars count as scalars
-  sc64_3 : Float -- `Float` is 64 bit
+  ptr_2 : { x : UInt64 // x > 0 } -- wrappers don't count as scalars
+  sc64_2 : Float -- `Float` is 64 bit
   sc8_1 : Bool
   sc16_1 : UInt16
   sc8_2 : UInt8
-  sc64_4 : UInt64
+  sc64_3 : UInt64
   usize_2 : USize
-  sc32_1 : Char -- trivial wrapper around `UInt32`
-  sc32_2 : UInt32
+  ptr_3 : Char -- trivial wrapper around `UInt32`
+  sc32_1 : UInt32
   sc16_2 : UInt16
 ```
 would get re-sorted into the following memory order:
 
 * `S.ptr_1` - `lean_ctor_get(val, 0)`
-* `S.usize_1` - `lean_ctor_get_usize(val, 1)`
-* `S.usize_2` - `lean_ctor_get_usize(val, 2)`
-* `S.sc64_1` - `lean_ctor_get_uint64(val, sizeof(void*)*3)`
-* `S.sc64_2` - `lean_ctor_get_uint64(val, sizeof(void*)*3 + 8)`
-* `S.sc64_3` - `lean_ctor_get_float(val, sizeof(void*)*3 + 16)`
-* `S.sc64_4` - `lean_ctor_get_uint64(val, sizeof(void*)*3 + 24)`
-* `S.sc32_1` - `lean_ctor_get_uint32(val, sizeof(void*)*3 + 32)`
-* `S.sc32_2` - `lean_ctor_get_uint32(val, sizeof(void*)*3 + 36)`
-* `S.sc16_1` - `lean_ctor_get_uint16(val, sizeof(void*)*3 + 40)`
-* `S.sc16_2` - `lean_ctor_get_uint16(val, sizeof(void*)*3 + 42)`
-* `S.sc8_1` - `lean_ctor_get_uint8(val, sizeof(void*)*3 + 44)`
-* `S.sc8_2` - `lean_ctor_get_uint8(val, sizeof(void*)*3 + 45)`
+* `S.ptr_2` - `lean_ctor_get(val, 1)`
+* `S.ptr_3` - `lean_ctor_get(val, 2)`
+* `S.usize_1` - `lean_ctor_get_usize(val, 3)`
+* `S.usize_2` - `lean_ctor_get_usize(val, 4)`
+* `S.sc64_1` - `lean_ctor_get_uint64(val, sizeof(void*)*5)`
+* `S.sc64_2` - `lean_ctor_get_float(val, sizeof(void*)*5 + 8)`
+* `S.sc64_3` - `lean_ctor_get_uint64(val, sizeof(void*)*5 + 16)`
+* `S.sc32_1` - `lean_ctor_get_uint32(val, sizeof(void*)*5 + 24)`
+* `S.sc16_1` - `lean_ctor_get_uint16(val, sizeof(void*)*5 + 28)`
+* `S.sc16_2` - `lean_ctor_get_uint16(val, sizeof(void*)*5 + 30)`
+* `S.sc8_1` - `lean_ctor_get_uint8(val, sizeof(void*)*5 + 32)`
+* `S.sc8_2` - `lean_ctor_get_uint8(val, sizeof(void*)*5 + 33)`
 
 ### Borrowing
 
@@ -131,21 +131,14 @@ Thus `[init]` functions are run iff their module is imported, regardless of whet
 
 The initializer for module `A.B` is called `initialize_A_B` and will automatically initialize any imported modules.
 Module initializers are idempotent (when run with the same `builtin` flag), but not thread-safe.
-
-**Important for process-related functionality**: If your application needs to use process-related functions from libuv, such as `Std.Internal.IO.Process.getProcessTitle` and `Std.Internal.IO.Process.setProcessTitle`, you must call `lean_setup_args(argc, argv)` (which returns a potentially modified `argv` that must be used in place of the original) **before** calling `lean_initialize()` or `lean_initialize_runtime_module()`. This sets up process handling capabilities correctly, which is essential for certain system-level operations that Lean's runtime may depend on.
-
 Together with initialization of the Lean runtime, you should execute code like the following exactly once before accessing any Lean declarations:
-
 ```c
 void lean_initialize_runtime_module();
 void lean_initialize();
-char ** lean_setup_args(int argc, char ** argv);
-
 lean_object * initialize_A_B(uint8_t builtin, lean_object *);
 lean_object * initialize_C(uint8_t builtin, lean_object *);
 ...
 
-argv = lean_setup_args(argc, argv); // if using process-related functionality
 lean_initialize_runtime_module();
 //lean_initialize();  // necessary (and replaces `lean_initialize_runtime_module`) if you (indirectly) access the `Lean` package
 

doc/dev/index.md

@@ -85,13 +85,5 @@ such that changing files in `Init` doesn't force a full rebuild of `Lean`.
 You can test a Lean PR against Mathlib and Batteries by rebasing your PR
 on to `nightly-with-mathlib` branch. (It is fine to force push after rebasing.)
 CI will generate a branch of Mathlib and Batteries called `lean-pr-testing-NNNN`
-on the `leanprover-community/mathlib4-nightly-testing` fork of Mathlib.
-This branch uses the toolchain for your PR, and will report back to the Lean PR with results from Mathlib CI.
+that uses the toolchain for your PR, and will report back to the Lean PR with results from Mathlib CI.
 See https://leanprover-community.github.io/contribute/tags_and_branches.html for more details.
-
-### Testing against the Lean Language Reference
-You can test a Lean PR against the reference manual by rebasing your PR
-on to `nightly-with-manual` branch. (It is fine to force push after rebasing.)
-CI will generate a branch of the reference manual called `lean-pr-testing-NNNN`
-in `leanprover/reference-manual`. This branch uses the toolchain for your PR,
-and will report back to the Lean PR with results from Mathlib CI.

doc/make/index.md

@@ -44,20 +44,15 @@ Useful CMake Configuration Settings
 Pass these along with the `cmake --preset release` command.
 There are also two alternative presets that combine some of these options you can use instead of `release`: `debug` and `sandebug` (sanitize + debug).
 
-* `-DCMAKE_BUILD_TYPE=`\
+* `-D CMAKE_BUILD_TYPE=`\
   Select the build type. Valid values are `RELEASE` (default), `DEBUG`,
   `RELWITHDEBINFO`, and `MINSIZEREL`.
 
-* `-DCMAKE_C_COMPILER=`\
-  `-DCMAKE_CXX_COMPILER=`\
+* `-D CMAKE_C_COMPILER=`\
+  `-D CMAKE_CXX_COMPILER=`\
   Select the C/C++ compilers to use. Official Lean releases currently use Clang;
   see also `.github/workflows/ci.yml` for the CI config.
 
-* `-DUSE_LAKE=ON`\
-  Experimental option to build the core libraries using Lake instead of `lean.mk`.  Caveats:
-  * As native code compilation is still handled by cmake, changes to stage0/ (such as from `git pull`) are picked up only when invoking the build via `make`, not via `Refresh Dependencies` in the editor.
-  * `USE_LAKE` is not yet compatible with `LAKE_ARTIFACT_CACHE`
-
 Lean will automatically use [CCache](https://ccache.dev/) if available to avoid
 redundant builds, especially after stage 0 has been updated.
 

doc/make/osx-10.9.md

@@ -1,4 +1,4 @@
-# Install Packages on OS X
+# Install Packages on OS X 14.5
 
 We assume that you are using [homebrew][homebrew] as a package manager.
 
@@ -6,23 +6,23 @@ We assume that you are using [homebrew][homebrew] as a package manager.
 
 ## Compilers
 
-You need a C++14-compatible compiler to build Lean. As of July
-2025, you have three options:
+You need a C++11-compatible compiler to build Lean. As of November
+2014, you have three options:
 
- - clang++ shipped with OSX (at time of writing v17.0.0)
- - clang++ via homebrew (at time of writing, v20.1.8)
- - gcc via homebrew (at time of writing, v15.1.0)
+ - clang++-3.5 (shipped with OSX, Apple LLVM version 6.0)
+ - gcc-4.9.1 (homebrew)
+ - clang++-3.5 (homebrew)
 
 We recommend to use Apple's clang++ because it is pre-shipped with OS
 X and requires no further installation.
 
-To install gcc via homebrew, please execute:
+To install gcc-4.9.1 via homebrew, please execute:
 ```bash
 brew install gcc
 ```
-To install clang via homebrew, please execute:
+To install clang++-3.5 via homebrew, please execute:
 ```bash
-brew install llvm lld
+brew install llvm
 ```
 To use compilers other than the default one (Apple's clang++), you
 need to use `-DCMAKE_CXX_COMPILER` option to specify the compiler

doc/std/grove/.gitignore

@@ -1,4 +0,0 @@
-/.lake
-!lake-manifest.json
-metadata.json
-invalidated.json

doc/std/grove/GroveStdlib/Generated.lean

@@ -1,22 +0,0 @@
-import Grove.Framework
-import GroveStdlib.Generated.«associative-query-operations»
-import GroveStdlib.Generated.«associative-creation-operations»
-import GroveStdlib.Generated.«associative-modification-operations»
-import GroveStdlib.Generated.«associative-create-then-query»
-import GroveStdlib.Generated.«associative-all-operations-covered»
-
-/-
-This file is autogenerated by grove. You can manually edit it, for example to resolve merge
-conflicts, but be careful.
--/
-
-open Grove.Framework Widget
-
-namespace GroveStdlib.Generated
-
-def restoreState : RestoreStateM Unit := do
-  «associative-query-operations».restoreState
-  «associative-creation-operations».restoreState
-  «associative-modification-operations».restoreState
-  «associative-create-then-query».restoreState
-  «associative-all-operations-covered».restoreState

doc/std/grove/GroveStdlib/Generated/associative-all-operations-covered.lean

@@ -1,34 +0,0 @@
-import Grove.Framework
-
-/-
-This file is autogenerated by grove. You can manually edit it, for example to resolve merge
-conflicts, but be careful.
--/
-
-open Grove.Framework Widget
-
-namespace GroveStdlib.Generated.«associative-all-operations-covered»
-
-def «all-covered» : Assertion.Fact where
-  widgetId := "associative-all-operations-covered"
-  factId := "all-covered"
-  assertionId := "all-covered"
-  state := {
-    assertionId := "all-covered"
-    description := "All operations should be covered"
-    passed := false
-    message := "There were 19697 operations that were not covered."
-  }
-  metadata := {
-    status := .bad
-    comment := "Still missing some!"
-  }
-
-def table : Assertion.Data  where
-  widgetId := "associative-all-operations-covered"
-  facts := #[
-    «all-covered»,
-  ]
-
-def restoreState : RestoreStateM Unit := do
-  addAssertion table

doc/std/grove/GroveStdlib/Generated/associative-create-then-query.lean

@@ -1,357 +0,0 @@
-import Grove.Framework
-
-/-
-This file is autogenerated by grove. You can manually edit it, for example to resolve merge
-conflicts, but be careful.
--/
-
-open Grove.Framework Widget
-
-namespace GroveStdlib.Generated.«associative-create-then-query»
-
-def «2cb3c441-9663-4ce7-9527-0f40fc29925a:::01f88623-fa5f-4380-9772-b30f2fec5c94:::Std.DHashMap::Std.DHashMap.Raw::Std.ExtDHashMap::Std.DTreeMap::Std.DTreeMap.Raw::Std.ExtDTreeMap» : Table.Fact .subexpression .subexpression .declaration where
-  widgetId := "associative-create-then-query"
-  factId := "2cb3c441-9663-4ce7-9527-0f40fc29925a:::01f88623-fa5f-4380-9772-b30f2fec5c94:::Std.DHashMap::Std.DHashMap.Raw::Std.ExtDHashMap::Std.DTreeMap::Std.DTreeMap.Raw::Std.ExtDTreeMap"
-  rowAssociationId := "2cb3c441-9663-4ce7-9527-0f40fc29925a"
-  columnAssociationId := "01f88623-fa5f-4380-9772-b30f2fec5c94"
-  selectedLayers := #["Std.DHashMap", "Std.DHashMap.Raw", "Std.ExtDHashMap", "Std.DTreeMap", "Std.DTreeMap.Raw", "Std.ExtDTreeMap", ]
-  layerStates := #[
-    {
-      layerIdentifier := "Std.DHashMap"
-      rowState := 
-        
-        some ⟨"Std.DHashMap.emptyWithCapacity", Grove.Framework.Subexpression.State.declaration
-          (Grove.Framework.Declaration.def
-            { name := `Std.DHashMap.emptyWithCapacity,
-              renderedStatement := "Std.DHashMap.emptyWithCapacity.{u, v} {α : Type u} {β : α → Type v} [BEq α] [Hashable α]\n  (capacity : Nat := 8) : Std.DHashMap α β",
-              isDeprecated := false })⟩
-        
-      columnState := 
-        
-        some ⟨"Std.DHashMap.isEmpty", Grove.Framework.Subexpression.State.declaration
-          (Grove.Framework.Declaration.def
-            { name := `Std.DHashMap.isEmpty,
-              renderedStatement := "Std.DHashMap.isEmpty.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α}\n  (m : Std.DHashMap α β) : Bool",
-              isDeprecated := false })⟩
-        
-      selectedCellStates := #[
-      ]
-    },
-    {
-      layerIdentifier := "Std.DHashMap.Raw"
-      rowState := 
-        
-        some ⟨"Std.DHashMap.Raw.emptyWithCapacity", Grove.Framework.Subexpression.State.declaration
-          (Grove.Framework.Declaration.def
-            { name := `Std.DHashMap.Raw.emptyWithCapacity,
-              renderedStatement := "Std.DHashMap.Raw.emptyWithCapacity.{u, v} {α : Type u} {β : α → Type v} (capacity : Nat := 8) :\n  Std.DHashMap.Raw α β",
-              isDeprecated := false })⟩
-        
-      columnState := 
-        
-        some ⟨"Std.DHashMap.Raw.isEmpty", Grove.Framework.Subexpression.State.declaration
-          (Grove.Framework.Declaration.def
-            { name := `Std.DHashMap.Raw.isEmpty,
-              renderedStatement := "Std.DHashMap.Raw.isEmpty.{u, v} {α : Type u} {β : α → Type v} (m : Std.DHashMap.Raw α β) : Bool",
-              isDeprecated := false })⟩
-        
-      selectedCellStates := #[
-      ]
-    },
-    {
-      layerIdentifier := "Std.ExtDHashMap"
-      rowState := 
-        
-        some ⟨"Std.ExtDHashMap.emptyWithCapacity", Grove.Framework.Subexpression.State.declaration
-          (Grove.Framework.Declaration.def
-            { name := `Std.ExtDHashMap.emptyWithCapacity,
-              renderedStatement := "Std.ExtDHashMap.emptyWithCapacity.{u, v} {α : Type u} {β : α → Type v} [BEq α] [Hashable α]\n  (capacity : Nat := 8) : Std.ExtDHashMap α β",
-              isDeprecated := false })⟩
-        
-      columnState := 
-        
-        some ⟨"Std.ExtDHashMap.isEmpty", Grove.Framework.Subexpression.State.declaration
-          (Grove.Framework.Declaration.def
-            { name := `Std.ExtDHashMap.isEmpty,
-              renderedStatement := "Std.ExtDHashMap.isEmpty.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α}\n  [EquivBEq α] [LawfulHashable α] (m : Std.ExtDHashMap α β) : Bool",
-              isDeprecated := false })⟩
-        
-      selectedCellStates := #[
-      ]
-    },
-    {
-      layerIdentifier := "Std.DTreeMap"
-      rowState := 
-        
-        some ⟨"Std.DTreeMap.empty", Grove.Framework.Subexpression.State.declaration
-          (Grove.Framework.Declaration.def
-            { name := `Std.DTreeMap.empty,
-              renderedStatement := "Std.DTreeMap.empty.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} :\n  Std.DTreeMap α β cmp",
-              isDeprecated := false })⟩
-        
-      columnState := 
-        
-        some ⟨"Std.DTreeMap.isEmpty", Grove.Framework.Subexpression.State.declaration
-          (Grove.Framework.Declaration.def
-            { name := `Std.DTreeMap.isEmpty,
-              renderedStatement := "Std.DTreeMap.isEmpty.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}\n  (t : Std.DTreeMap α β cmp) : Bool",
-              isDeprecated := false })⟩
-        
-      selectedCellStates := #[
-      ]
-    },
-    {
-      layerIdentifier := "Std.DTreeMap.Raw"
-      rowState := 
-        
-        some ⟨"Std.DTreeMap.Raw.empty", Grove.Framework.Subexpression.State.declaration
-          (Grove.Framework.Declaration.def
-            { name := `Std.DTreeMap.Raw.empty,
-              renderedStatement := "Std.DTreeMap.Raw.empty.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} :\n  Std.DTreeMap.Raw α β cmp",
-              isDeprecated := false })⟩
-        
-      columnState := 
-        
-        some ⟨"Std.DTreeMap.Raw.isEmpty", Grove.Framework.Subexpression.State.declaration
-          (Grove.Framework.Declaration.def
-            { name := `Std.DTreeMap.Raw.isEmpty,
-              renderedStatement := "Std.DTreeMap.Raw.isEmpty.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}\n  (t : Std.DTreeMap.Raw α β cmp) : Bool",
-              isDeprecated := false })⟩
-        
-      selectedCellStates := #[
-      ]
-    },
-    {
-      layerIdentifier := "Std.ExtDTreeMap"
-      rowState := 
-        
-        some ⟨"Std.ExtDTreeMap.empty", Grove.Framework.Subexpression.State.declaration
-          (Grove.Framework.Declaration.def
-            { name := `Std.ExtDTreeMap.empty,
-              renderedStatement := "Std.ExtDTreeMap.empty.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} :\n  Std.ExtDTreeMap α β cmp",
-              isDeprecated := false })⟩
-        
-      columnState := 
-        
-        some ⟨"Std.ExtDTreeMap.isEmpty", Grove.Framework.Subexpression.State.declaration
-          (Grove.Framework.Declaration.def
-            { name := `Std.ExtDTreeMap.isEmpty,
-              renderedStatement := "Std.ExtDTreeMap.isEmpty.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}\n  (t : Std.ExtDTreeMap α β cmp) : Bool",
-              isDeprecated := false })⟩
-        
-      selectedCellStates := #[
-      ]
-    },
-  ]
-  metadata := {
-    status := .done
-    comment := "Not necessary for `ExtDHashMap` because of simp lemma turning into varno"
-  }
-
-def «5ceaa26a-d2cb-4df3-9ac8-b5c11db2ae9d:::01f88623-fa5f-4380-9772-b30f2fec5c94:::Std.DHashMap::Std.DHashMap.Raw::Std.ExtDHashMap::Std.DTreeMap::Std.DTreeMap.Raw::Std.ExtDTreeMap» : Table.Fact .subexpression .subexpression .declaration where
-  widgetId := "associative-create-then-query"
-  factId := "5ceaa26a-d2cb-4df3-9ac8-b5c11db2ae9d:::01f88623-fa5f-4380-9772-b30f2fec5c94:::Std.DHashMap::Std.DHashMap.Raw::Std.ExtDHashMap::Std.DTreeMap::Std.DTreeMap.Raw::Std.ExtDTreeMap"
-  rowAssociationId := "5ceaa26a-d2cb-4df3-9ac8-b5c11db2ae9d"
-  columnAssociationId := "01f88623-fa5f-4380-9772-b30f2fec5c94"
-  selectedLayers := #["Std.DHashMap", "Std.DHashMap.Raw", "Std.ExtDHashMap", "Std.DTreeMap", "Std.DTreeMap.Raw", "Std.ExtDTreeMap", ]
-  layerStates := #[
-    {
-      layerIdentifier := "Std.DHashMap"
-      rowState := 
-        
-        some ⟨"app (EmptyCollection.emptyCollection) (Std.DHashMap*)", Grove.Framework.Subexpression.State.predicate
-          { key := "app (EmptyCollection.emptyCollection) (Std.DHashMap*)", displayShort := "∅" }⟩
-        
-      columnState := 
-        
-        some ⟨"Std.DHashMap.isEmpty", Grove.Framework.Subexpression.State.declaration
-          (Grove.Framework.Declaration.def
-            { name := `Std.DHashMap.isEmpty,
-              renderedStatement := "Std.DHashMap.isEmpty.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α}\n  (m : Std.DHashMap α β) : Bool",
-              isDeprecated := false })⟩
-        
-      selectedCellStates := #[
-        ⟨"Std.DHashMap.isEmpty_empty", Grove.Framework.Declaration.thm
-  { name := `Std.DHashMap.isEmpty_empty,
-    renderedStatement := "Std.DHashMap.isEmpty_empty.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} :\n  ∅.isEmpty = true",
-    isSimp := true,
-    isDeprecated := false }⟩
-,
-      ]
-    },
-    {
-      layerIdentifier := "Std.DHashMap.Raw"
-      rowState := 
-        
-        some ⟨"app (EmptyCollection.emptyCollection) (Std.DHashMap.Raw*)", Grove.Framework.Subexpression.State.predicate
-          { key := "app (EmptyCollection.emptyCollection) (Std.DHashMap.Raw*)", displayShort := "∅" }⟩
-        
-      columnState := 
-        
-        some ⟨"Std.DHashMap.Raw.isEmpty", Grove.Framework.Subexpression.State.declaration
-          (Grove.Framework.Declaration.def
-            { name := `Std.DHashMap.Raw.isEmpty,
-              renderedStatement := "Std.DHashMap.Raw.isEmpty.{u, v} {α : Type u} {β : α → Type v} (m : Std.DHashMap.Raw α β) : Bool",
-              isDeprecated := false })⟩
-        
-      selectedCellStates := #[
-        ⟨"Std.DHashMap.Raw.isEmpty_emptyc", Grove.Framework.Declaration.thm
-  { name := `Std.DHashMap.Raw.isEmpty_emptyc,
-    renderedStatement := "Std.DHashMap.Raw.isEmpty_emptyc.{u_1, u_2} {α : Type u_1} {β : α → Type u_2} [BEq α] [Hashable α] :\n  ∅.isEmpty = true",
-    isSimp := false,
-    isDeprecated := true }⟩
-,
-      ]
-    },
-    {
-      layerIdentifier := "Std.ExtDHashMap"
-      rowState := 
-        
-        some ⟨"app (EmptyCollection.emptyCollection) (Std.ExtDHashMap*)", Grove.Framework.Subexpression.State.predicate
-          { key := "app (EmptyCollection.emptyCollection) (Std.ExtDHashMap*)", displayShort := "∅" }⟩
-        
-      columnState := 
-        
-        some ⟨"Std.ExtDHashMap.isEmpty", Grove.Framework.Subexpression.State.declaration
-          (Grove.Framework.Declaration.def
-            { name := `Std.ExtDHashMap.isEmpty,
-              renderedStatement := "Std.ExtDHashMap.isEmpty.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α}\n  [EquivBEq α] [LawfulHashable α] (m : Std.ExtDHashMap α β) : Bool",
-              isDeprecated := false })⟩
-        
-      selectedCellStates := #[
-      ]
-    },
-    {
-      layerIdentifier := "Std.DTreeMap"
-      rowState := 
-        
-        some ⟨"app (EmptyCollection.emptyCollection) (Std.DTreeMap*)", Grove.Framework.Subexpression.State.predicate
-          { key := "app (EmptyCollection.emptyCollection) (Std.DTreeMap*)", displayShort := "∅" }⟩
-        
-      columnState := 
-        
-        some ⟨"Std.DTreeMap.isEmpty", Grove.Framework.Subexpression.State.declaration
-          (Grove.Framework.Declaration.def
-            { name := `Std.DTreeMap.isEmpty,
-              renderedStatement := "Std.DTreeMap.isEmpty.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}\n  (t : Std.DTreeMap α β cmp) : Bool",
-              isDeprecated := false })⟩
-        
-      selectedCellStates := #[
-        ⟨"Std.DTreeMap.isEmpty_emptyc", Grove.Framework.Declaration.thm
-  { name := `Std.DTreeMap.isEmpty_emptyc,
-    renderedStatement := "Std.DTreeMap.isEmpty_emptyc.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} :\n  ∅.isEmpty = true",
-    isSimp := true,
-    isDeprecated := false }⟩
-,
-      ]
-    },
-    {
-      layerIdentifier := "Std.DTreeMap.Raw"
-      rowState := 
-        
-        some ⟨"app (EmptyCollection.emptyCollection) (Std.DTreeMap.Raw*)", Grove.Framework.Subexpression.State.predicate
-          { key := "app (EmptyCollection.emptyCollection) (Std.DTreeMap.Raw*)", displayShort := "∅" }⟩
-        
-      columnState := 
-        
-        some ⟨"Std.DTreeMap.Raw.isEmpty", Grove.Framework.Subexpression.State.declaration
-          (Grove.Framework.Declaration.def
-            { name := `Std.DTreeMap.Raw.isEmpty,
-              renderedStatement := "Std.DTreeMap.Raw.isEmpty.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}\n  (t : Std.DTreeMap.Raw α β cmp) : Bool",
-              isDeprecated := false })⟩
-        
-      selectedCellStates := #[
-        ⟨"Std.DTreeMap.Raw.isEmpty_emptyc", Grove.Framework.Declaration.thm
-  { name := `Std.DTreeMap.Raw.isEmpty_emptyc,
-    renderedStatement := "Std.DTreeMap.Raw.isEmpty_emptyc.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} :\n  ∅.isEmpty = true",
-    isSimp := true,
-    isDeprecated := false }⟩
-,
-      ]
-    },
-    {
-      layerIdentifier := "Std.ExtDTreeMap"
-      rowState := 
-        
-        some ⟨"app (EmptyCollection.emptyCollection) (Std.ExtDTreeMap*)", Grove.Framework.Subexpression.State.predicate
-          { key := "app (EmptyCollection.emptyCollection) (Std.ExtDTreeMap*)", displayShort := "∅" }⟩
-        
-      columnState := 
-        
-        some ⟨"Std.ExtDTreeMap.isEmpty", Grove.Framework.Subexpression.State.declaration
-          (Grove.Framework.Declaration.def
-            { name := `Std.ExtDTreeMap.isEmpty,
-              renderedStatement := "Std.ExtDTreeMap.isEmpty.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}\n  (t : Std.ExtDTreeMap α β cmp) : Bool",
-              isDeprecated := false })⟩
-        
-      selectedCellStates := #[
-        ⟨"Std.ExtDTreeMap.isEmpty_empty", Grove.Framework.Declaration.thm
-  { name := `Std.ExtDTreeMap.isEmpty_empty,
-    renderedStatement := "Std.ExtDTreeMap.isEmpty_empty.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} :\n  ∅.isEmpty = true",
-    isSimp := true,
-    isDeprecated := false }⟩
-,
-      ]
-    },
-  ]
-  metadata := {
-    status := .bad
-    comment := "Missing for `ExtDHashMap`"
-  }
-
-def table : Table.Data .subexpression .subexpression .declaration where
-  widgetId := "associative-create-then-query"
-  selectedRowAssociations := #["2cb3c441-9663-4ce7-9527-0f40fc29925a", "7743a485-024d-43b6-bd5f-ebd3182eb94d", "5ceaa26a-d2cb-4df3-9ac8-b5c11db2ae9d", ]
-  selectedColumnAssociations := #["01f88623-fa5f-4380-9772-b30f2fec5c94", "f084f852-af71-45b6-8ab3-d251a8144f72", ]
-  selectedLayers := #["Std.DHashMap", "Std.DHashMap.Raw", "Std.ExtDHashMap", "Std.DTreeMap", "Std.DTreeMap.Raw", "Std.ExtDTreeMap", ]
-  selectedCellOptions := #[
-    {
-      layerIdentifier := "Std.DHashMap"
-      rowValue := "2cb3c441-9663-4ce7-9527-0f40fc29925a"
-      columnValue := "01f88623-fa5f-4380-9772-b30f2fec5c94"
-      selectedCellOptions := #["Std.DHashMap.isEmpty_emptyWithCapacity", ]
-    },
-    {
-      layerIdentifier := "Std.DHashMap.Raw"
-      rowValue := "2cb3c441-9663-4ce7-9527-0f40fc29925a"
-      columnValue := "01f88623-fa5f-4380-9772-b30f2fec5c94"
-      selectedCellOptions := #["Std.DHashMap.Raw.isEmpty_emptyWithCapacity", ]
-    },
-    {
-      layerIdentifier := "Std.DHashMap"
-      rowValue := "5ceaa26a-d2cb-4df3-9ac8-b5c11db2ae9d"
-      columnValue := "01f88623-fa5f-4380-9772-b30f2fec5c94"
-      selectedCellOptions := #["Std.DHashMap.isEmpty_empty", ]
-    },
-    {
-      layerIdentifier := "Std.DHashMap.Raw"
-      rowValue := "5ceaa26a-d2cb-4df3-9ac8-b5c11db2ae9d"
-      columnValue := "01f88623-fa5f-4380-9772-b30f2fec5c94"
-      selectedCellOptions := #["Std.DHashMap.Raw.isEmpty_emptyc", ]
-    },
-    {
-      layerIdentifier := "Std.DTreeMap"
-      rowValue := "5ceaa26a-d2cb-4df3-9ac8-b5c11db2ae9d"
-      columnValue := "01f88623-fa5f-4380-9772-b30f2fec5c94"
-      selectedCellOptions := #["Std.DTreeMap.isEmpty_emptyc", ]
-    },
-    {
-      layerIdentifier := "Std.DTreeMap.Raw"
-      rowValue := "5ceaa26a-d2cb-4df3-9ac8-b5c11db2ae9d"
-      columnValue := "01f88623-fa5f-4380-9772-b30f2fec5c94"
-      selectedCellOptions := #["Std.DTreeMap.Raw.isEmpty_emptyc", ]
-    },
-    {
-      layerIdentifier := "Std.ExtDTreeMap"
-      rowValue := "5ceaa26a-d2cb-4df3-9ac8-b5c11db2ae9d"
-      columnValue := "01f88623-fa5f-4380-9772-b30f2fec5c94"
-      selectedCellOptions := #["Std.ExtDTreeMap.isEmpty_empty", ]
-    },
-  ]
-  facts := #[
-    «2cb3c441-9663-4ce7-9527-0f40fc29925a:::01f88623-fa5f-4380-9772-b30f2fec5c94:::Std.DHashMap::Std.DHashMap.Raw::Std.ExtDHashMap::Std.DTreeMap::Std.DTreeMap.Raw::Std.ExtDTreeMap»,
-    «5ceaa26a-d2cb-4df3-9ac8-b5c11db2ae9d:::01f88623-fa5f-4380-9772-b30f2fec5c94:::Std.DHashMap::Std.DHashMap.Raw::Std.ExtDHashMap::Std.DTreeMap::Std.DTreeMap.Raw::Std.ExtDTreeMap»,
-  ]
-
-def restoreState : RestoreStateM Unit := do
-  addTable table

doc/std/grove/GroveStdlib/Generated/associative-creation-operations.lean

@@ -1,216 +0,0 @@
-import Grove.Framework
-
-/-
-This file is autogenerated by grove. You can manually edit it, for example to resolve merge
-conflicts, but be careful.
--/
-
-open Grove.Framework Widget
-
-namespace GroveStdlib.Generated.«associative-creation-operations»
-
-def «2cb3c441-9663-4ce7-9527-0f40fc29925a» : AssociationTable.Fact .subexpression where
-  widgetId := "associative-creation-operations"
-  factId := "2cb3c441-9663-4ce7-9527-0f40fc29925a"
-  rowId := "2cb3c441-9663-4ce7-9527-0f40fc29925a"
-  rowState := #[⟨"Std.DHashMap", "Std.DHashMap.emptyWithCapacity", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.DHashMap.emptyWithCapacity,
-      renderedStatement := "Std.DHashMap.emptyWithCapacity.{u, v} {α : Type u} {β : α → Type v} [BEq α] [Hashable α]\n  (capacity : Nat := 8) : Std.DHashMap α β",
-      isDeprecated := false })⟩,⟨"Std.DHashMap.Raw", "Std.DHashMap.Raw.emptyWithCapacity", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.DHashMap.Raw.emptyWithCapacity,
-      renderedStatement := "Std.DHashMap.Raw.emptyWithCapacity.{u, v} {α : Type u} {β : α → Type v} (capacity : Nat := 8) :\n  Std.DHashMap.Raw α β",
-      isDeprecated := false })⟩,⟨"Std.ExtDHashMap", "Std.ExtDHashMap.emptyWithCapacity", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.ExtDHashMap.emptyWithCapacity,
-      renderedStatement := "Std.ExtDHashMap.emptyWithCapacity.{u, v} {α : Type u} {β : α → Type v} [BEq α] [Hashable α]\n  (capacity : Nat := 8) : Std.ExtDHashMap α β",
-      isDeprecated := false })⟩,⟨"Std.DTreeMap", "Std.DTreeMap.empty", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.DTreeMap.empty,
-      renderedStatement := "Std.DTreeMap.empty.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} :\n  Std.DTreeMap α β cmp",
-      isDeprecated := false })⟩,⟨"Std.DTreeMap.Raw", "Std.DTreeMap.Raw.empty", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.DTreeMap.Raw.empty,
-      renderedStatement := "Std.DTreeMap.Raw.empty.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} :\n  Std.DTreeMap.Raw α β cmp",
-      isDeprecated := false })⟩,⟨"Std.ExtDTreeMap", "Std.ExtDTreeMap.empty", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.ExtDTreeMap.empty,
-      renderedStatement := "Std.ExtDTreeMap.empty.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} :\n  Std.ExtDTreeMap α β cmp",
-      isDeprecated := false })⟩,⟨"Std.HashMap", "Std.HashMap.emptyWithCapacity", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.HashMap.emptyWithCapacity,
-      renderedStatement := "Std.HashMap.emptyWithCapacity.{u, v} {α : Type u} {β : Type v} [BEq α] [Hashable α]\n  (capacity : Nat := 8) : Std.HashMap α β",
-      isDeprecated := false })⟩,⟨"Std.HashMap.Raw", "Std.HashMap.Raw.emptyWithCapacity", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.HashMap.Raw.emptyWithCapacity,
-      renderedStatement := "Std.HashMap.Raw.emptyWithCapacity.{u, v} {α : Type u} {β : Type v} (capacity : Nat := 8) :\n  Std.HashMap.Raw α β",
-      isDeprecated := false })⟩,⟨"Std.ExtHashMap", "Std.ExtHashMap.emptyWithCapacity", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.ExtHashMap.emptyWithCapacity,
-      renderedStatement := "Std.ExtHashMap.emptyWithCapacity.{u, v} {α : Type u} {β : Type v} [BEq α] [Hashable α]\n  (capacity : Nat := 8) : Std.ExtHashMap α β",
-      isDeprecated := false })⟩,⟨"Std.TreeMap", "Std.TreeMap.empty", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.TreeMap.empty,
-      renderedStatement := "Std.TreeMap.empty.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering} : Std.TreeMap α β cmp",
-      isDeprecated := false })⟩,⟨"Std.TreeMap.Raw", "Std.TreeMap.Raw.empty", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.TreeMap.Raw.empty,
-      renderedStatement := "Std.TreeMap.Raw.empty.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering} :\n  Std.TreeMap.Raw α β cmp",
-      isDeprecated := false })⟩,⟨"Std.ExtTreeMap", "Std.ExtTreeMap.empty", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.ExtTreeMap.empty,
-      renderedStatement := "Std.ExtTreeMap.empty.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering} :\n  Std.ExtTreeMap α β cmp",
-      isDeprecated := false })⟩,⟨"Std.HashSet", "Std.HashSet.emptyWithCapacity", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.HashSet.emptyWithCapacity,
-      renderedStatement := "Std.HashSet.emptyWithCapacity.{u} {α : Type u} [BEq α] [Hashable α] (capacity : Nat := 8) :\n  Std.HashSet α",
-      isDeprecated := false })⟩,⟨"Std.HashSet.Raw", "Std.HashSet.Raw.emptyWithCapacity", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.HashSet.Raw.emptyWithCapacity,
-      renderedStatement := "Std.HashSet.Raw.emptyWithCapacity.{u} {α : Type u} (capacity : Nat := 8) : Std.HashSet.Raw α",
-      isDeprecated := false })⟩,⟨"Std.ExtHashSet", "Std.ExtHashSet.emptyWithCapacity", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.ExtHashSet.emptyWithCapacity,
-      renderedStatement := "Std.ExtHashSet.emptyWithCapacity.{u} {α : Type u} [BEq α] [Hashable α] (capacity : Nat := 8) :\n  Std.ExtHashSet α",
-      isDeprecated := false })⟩,⟨"Std.TreeSet", "Std.TreeSet.empty", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.TreeSet.empty,
-      renderedStatement := "Std.TreeSet.empty.{u} {α : Type u} {cmp : α → α → Ordering} : Std.TreeSet α cmp",
-      isDeprecated := false })⟩,⟨"Std.TreeSet.Raw", "Std.TreeSet.Raw.empty", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.TreeSet.Raw.empty,
-      renderedStatement := "Std.TreeSet.Raw.empty.{u} {α : Type u} {cmp : α → α → Ordering} : Std.TreeSet.Raw α cmp",
-      isDeprecated := false })⟩,⟨"Std.ExtTreeSet", "Std.ExtTreeSet.empty", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.ExtTreeSet.empty,
-      renderedStatement := "Std.ExtTreeSet.empty.{u} {α : Type u} {cmp : α → α → Ordering} : Std.ExtTreeSet α cmp",
-      isDeprecated := false })⟩,]
-  metadata := {
-    status := .done
-    comment := ""
-  }
-def «7743a485-024d-43b6-bd5f-ebd3182eb94d» : AssociationTable.Fact .subexpression where
-  widgetId := "associative-creation-operations"
-  factId := "7743a485-024d-43b6-bd5f-ebd3182eb94d"
-  rowId := "7743a485-024d-43b6-bd5f-ebd3182eb94d"
-  rowState := #[⟨"Std.DHashMap", "Std.DHashMap.ofList", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.DHashMap.ofList,
-      renderedStatement := "Std.DHashMap.ofList.{u, v} {α : Type u} {β : α → Type v} [BEq α] [Hashable α]\n  (l : List ((a : α) × β a)) : Std.DHashMap α β",
-      isDeprecated := false })⟩,⟨"Std.DHashMap.Raw", "Std.DHashMap.Raw.ofList", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.DHashMap.Raw.ofList,
-      renderedStatement := "Std.DHashMap.Raw.ofList.{u, v} {α : Type u} {β : α → Type v} [BEq α] [Hashable α]\n  (l : List ((a : α) × β a)) : Std.DHashMap.Raw α β",
-      isDeprecated := false })⟩,⟨"Std.ExtDHashMap", "Std.ExtDHashMap.ofList", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.ExtDHashMap.ofList,
-      renderedStatement := "Std.ExtDHashMap.ofList.{u, v} {α : Type u} {β : α → Type v} [BEq α] [Hashable α]\n  (l : List ((a : α) × β a)) : Std.ExtDHashMap α β",
-      isDeprecated := false })⟩,⟨"Std.DTreeMap", "Std.DTreeMap.ofList", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.DTreeMap.ofList,
-      renderedStatement := "Std.DTreeMap.ofList.{u, v} {α : Type u} {β : α → Type v} (l : List ((a : α) × β a))\n  (cmp : α → α → Ordering := by exact compare) : Std.DTreeMap α β cmp",
-      isDeprecated := false })⟩,⟨"Std.DTreeMap.Raw", "Std.DTreeMap.Raw.ofList", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.DTreeMap.Raw.ofList,
-      renderedStatement := "Std.DTreeMap.Raw.ofList.{u, v} {α : Type u} {β : α → Type v} (l : List ((a : α) × β a))\n  (cmp : α → α → Ordering := by exact compare) : Std.DTreeMap.Raw α β cmp",
-      isDeprecated := false })⟩,⟨"Std.ExtDTreeMap", "Std.ExtDTreeMap.ofList", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.ExtDTreeMap.ofList,
-      renderedStatement := "Std.ExtDTreeMap.ofList.{u, v} {α : Type u} {β : α → Type v} (l : List ((a : α) × β a))\n  (cmp : α → α → Ordering := by exact compare) : Std.ExtDTreeMap α β cmp",
-      isDeprecated := false })⟩,⟨"Std.HashMap", "Std.HashMap.ofList", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.HashMap.ofList,
-      renderedStatement := "Std.HashMap.ofList.{u, v} {α : Type u} {β : Type v} [BEq α] [Hashable α] (l : List (α × β)) :\n  Std.HashMap α β",
-      isDeprecated := false })⟩,⟨"Std.HashMap.Raw", "Std.HashMap.Raw.ofList", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.HashMap.Raw.ofList,
-      renderedStatement := "Std.HashMap.Raw.ofList.{u, v} {α : Type u} {β : Type v} [BEq α] [Hashable α] (l : List (α × β)) :\n  Std.HashMap.Raw α β",
-      isDeprecated := false })⟩,⟨"Std.ExtHashMap", "Std.ExtHashMap.ofList", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.ExtHashMap.ofList,
-      renderedStatement := "Std.ExtHashMap.ofList.{u, v} {α : Type u} {β : Type v} [BEq α] [Hashable α] (l : List (α × β)) :\n  Std.ExtHashMap α β",
-      isDeprecated := false })⟩,⟨"Std.TreeMap", "Std.TreeMap.ofList", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.TreeMap.ofList,
-      renderedStatement := "Std.TreeMap.ofList.{u, v} {α : Type u} {β : Type v} (l : List (α × β))\n  (cmp : α → α → Ordering := by exact compare) : Std.TreeMap α β cmp",
-      isDeprecated := false })⟩,⟨"Std.TreeMap.Raw", "Std.TreeMap.Raw.ofList", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.TreeMap.Raw.ofList,
-      renderedStatement := "Std.TreeMap.Raw.ofList.{u, v} {α : Type u} {β : Type v} (l : List (α × β))\n  (cmp : α → α → Ordering := by exact compare) : Std.TreeMap.Raw α β cmp",
-      isDeprecated := false })⟩,⟨"Std.ExtTreeMap", "Std.ExtTreeMap.ofList", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.ExtTreeMap.ofList,
-      renderedStatement := "Std.ExtTreeMap.ofList.{u, v} {α : Type u} {β : Type v} (l : List (α × β))\n  (cmp : α → α → Ordering := by exact compare) : Std.ExtTreeMap α β cmp",
-      isDeprecated := false })⟩,⟨"Std.HashSet", "Std.HashSet.ofList", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.HashSet.ofList,
-      renderedStatement := "Std.HashSet.ofList.{u} {α : Type u} [BEq α] [Hashable α] (l : List α) : Std.HashSet α",
-      isDeprecated := false })⟩,⟨"Std.HashSet.Raw", "Std.HashSet.Raw.ofList", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.HashSet.Raw.ofList,
-      renderedStatement := "Std.HashSet.Raw.ofList.{u} {α : Type u} [BEq α] [Hashable α] (l : List α) : Std.HashSet.Raw α",
-      isDeprecated := false })⟩,⟨"Std.ExtHashSet", "Std.ExtHashSet.ofList", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.ExtHashSet.ofList,
-      renderedStatement := "Std.ExtHashSet.ofList.{u} {α : Type u} [BEq α] [Hashable α] (l : List α) : Std.ExtHashSet α",
-      isDeprecated := false })⟩,⟨"Std.TreeSet", "Std.TreeSet.ofList", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.TreeSet.ofList,
-      renderedStatement := "Std.TreeSet.ofList.{u} {α : Type u} (l : List α) (cmp : α → α → Ordering := by exact compare) :\n  Std.TreeSet α cmp",
-      isDeprecated := false })⟩,⟨"Std.TreeSet.Raw", "Std.TreeSet.Raw.ofList", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.TreeSet.Raw.ofList,
-      renderedStatement := "Std.TreeSet.Raw.ofList.{u} {α : Type u} (l : List α) (cmp : α → α → Ordering := by exact compare) :\n  Std.TreeSet.Raw α cmp",
-      isDeprecated := false })⟩,⟨"Std.ExtTreeSet", "Std.ExtTreeSet.ofList", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.ExtTreeSet.ofList,
-      renderedStatement := "Std.ExtTreeSet.ofList.{u} {α : Type u} (l : List α) (cmp : α → α → Ordering := by exact compare) :\n  Std.ExtTreeSet α cmp",
-      isDeprecated := false })⟩,]
-  metadata := {
-    status := .done
-    comment := ""
-  }
-def «5ceaa26a-d2cb-4df3-9ac8-b5c11db2ae9d» : AssociationTable.Fact .subexpression where
-  widgetId := "associative-creation-operations"
-  factId := "5ceaa26a-d2cb-4df3-9ac8-b5c11db2ae9d"
-  rowId := "5ceaa26a-d2cb-4df3-9ac8-b5c11db2ae9d"
-  rowState := #[⟨"Std.DHashMap", "app (EmptyCollection.emptyCollection) (Std.DHashMap*)", Grove.Framework.Subexpression.State.predicate
-  { key := "app (EmptyCollection.emptyCollection) (Std.DHashMap*)", displayShort := "∅" }⟩,⟨"Std.DHashMap.Raw", "app (EmptyCollection.emptyCollection) (Std.DHashMap.Raw*)", Grove.Framework.Subexpression.State.predicate
-  { key := "app (EmptyCollection.emptyCollection) (Std.DHashMap.Raw*)", displayShort := "∅" }⟩,⟨"Std.ExtDHashMap", "app (EmptyCollection.emptyCollection) (Std.ExtDHashMap*)", Grove.Framework.Subexpression.State.predicate
-  { key := "app (EmptyCollection.emptyCollection) (Std.ExtDHashMap*)", displayShort := "∅" }⟩,⟨"Std.DTreeMap", "app (EmptyCollection.emptyCollection) (Std.DTreeMap*)", Grove.Framework.Subexpression.State.predicate
-  { key := "app (EmptyCollection.emptyCollection) (Std.DTreeMap*)", displayShort := "∅" }⟩,⟨"Std.DTreeMap.Raw", "app (EmptyCollection.emptyCollection) (Std.DTreeMap.Raw*)", Grove.Framework.Subexpression.State.predicate
-  { key := "app (EmptyCollection.emptyCollection) (Std.DTreeMap.Raw*)", displayShort := "∅" }⟩,⟨"Std.ExtDTreeMap", "app (EmptyCollection.emptyCollection) (Std.ExtDTreeMap*)", Grove.Framework.Subexpression.State.predicate
-  { key := "app (EmptyCollection.emptyCollection) (Std.ExtDTreeMap*)", displayShort := "∅" }⟩,⟨"Std.HashMap", "app (EmptyCollection.emptyCollection) (Std.HashMap*)", Grove.Framework.Subexpression.State.predicate
-  { key := "app (EmptyCollection.emptyCollection) (Std.HashMap*)", displayShort := "∅" }⟩,⟨"Std.HashMap.Raw", "app (EmptyCollection.emptyCollection) (Std.HashMap.Raw*)", Grove.Framework.Subexpression.State.predicate
-  { key := "app (EmptyCollection.emptyCollection) (Std.HashMap.Raw*)", displayShort := "∅" }⟩,⟨"Std.ExtHashMap", "app (EmptyCollection.emptyCollection) (Std.ExtHashMap*)", Grove.Framework.Subexpression.State.predicate
-  { key := "app (EmptyCollection.emptyCollection) (Std.ExtHashMap*)", displayShort := "∅" }⟩,⟨"Std.TreeMap", "app (EmptyCollection.emptyCollection) (Std.TreeMap*)", Grove.Framework.Subexpression.State.predicate
-  { key := "app (EmptyCollection.emptyCollection) (Std.TreeMap*)", displayShort := "∅" }⟩,⟨"Std.TreeMap.Raw", "app (EmptyCollection.emptyCollection) (Std.TreeMap.Raw*)", Grove.Framework.Subexpression.State.predicate
-  { key := "app (EmptyCollection.emptyCollection) (Std.TreeMap.Raw*)", displayShort := "∅" }⟩,⟨"Std.ExtTreeMap", "app (EmptyCollection.emptyCollection) (Std.ExtTreeMap*)", Grove.Framework.Subexpression.State.predicate
-  { key := "app (EmptyCollection.emptyCollection) (Std.ExtTreeMap*)", displayShort := "∅" }⟩,⟨"Std.HashSet", "app (EmptyCollection.emptyCollection) (Std.HashSet*)", Grove.Framework.Subexpression.State.predicate
-  { key := "app (EmptyCollection.emptyCollection) (Std.HashSet*)", displayShort := "∅" }⟩,⟨"Std.HashSet.Raw", "app (EmptyCollection.emptyCollection) (Std.HashSet.Raw*)", Grove.Framework.Subexpression.State.predicate
-  { key := "app (EmptyCollection.emptyCollection) (Std.HashSet.Raw*)", displayShort := "∅" }⟩,⟨"Std.ExtHashSet", "app (EmptyCollection.emptyCollection) (Std.ExtHashSet*)", Grove.Framework.Subexpression.State.predicate
-  { key := "app (EmptyCollection.emptyCollection) (Std.ExtHashSet*)", displayShort := "∅" }⟩,⟨"Std.TreeSet", "app (EmptyCollection.emptyCollection) (Std.TreeSet*)", Grove.Framework.Subexpression.State.predicate
-  { key := "app (EmptyCollection.emptyCollection) (Std.TreeSet*)", displayShort := "∅" }⟩,⟨"Std.TreeSet.Raw", "app (EmptyCollection.emptyCollection) (Std.TreeSet.Raw*)", Grove.Framework.Subexpression.State.predicate
-  { key := "app (EmptyCollection.emptyCollection) (Std.TreeSet.Raw*)", displayShort := "∅" }⟩,⟨"Std.ExtTreeSet", "app (EmptyCollection.emptyCollection) (Std.ExtTreeSet*)", Grove.Framework.Subexpression.State.predicate
-  { key := "app (EmptyCollection.emptyCollection) (Std.ExtTreeSet*)", displayShort := "∅" }⟩,]
-  metadata := {
-    status := .done
-    comment := ""
-  }
-
-def table : AssociationTable.Data .subexpression where
-  widgetId := "associative-creation-operations"
-  rows := #[
-    ⟨"2cb3c441-9663-4ce7-9527-0f40fc29925a", "empty", #[⟨"Std.DHashMap", "Std.DHashMap.emptyWithCapacity"⟩,⟨"Std.DHashMap.Raw", "Std.DHashMap.Raw.emptyWithCapacity"⟩,⟨"Std.ExtDHashMap", "Std.ExtDHashMap.emptyWithCapacity"⟩,⟨"Std.DTreeMap", "Std.DTreeMap.empty"⟩,⟨"Std.DTreeMap.Raw", "Std.DTreeMap.Raw.empty"⟩,⟨"Std.ExtDTreeMap", "Std.ExtDTreeMap.empty"⟩,⟨"Std.HashMap", "Std.HashMap.emptyWithCapacity"⟩,⟨"Std.HashMap.Raw", "Std.HashMap.Raw.emptyWithCapacity"⟩,⟨"Std.ExtHashMap", "Std.ExtHashMap.emptyWithCapacity"⟩,⟨"Std.TreeMap", "Std.TreeMap.empty"⟩,⟨"Std.TreeMap.Raw", "Std.TreeMap.Raw.empty"⟩,⟨"Std.ExtTreeMap", "Std.ExtTreeMap.empty"⟩,⟨"Std.HashSet", "Std.HashSet.emptyWithCapacity"⟩,⟨"Std.HashSet.Raw", "Std.HashSet.Raw.emptyWithCapacity"⟩,⟨"Std.ExtHashSet", "Std.ExtHashSet.emptyWithCapacity"⟩,⟨"Std.TreeSet", "Std.TreeSet.empty"⟩,⟨"Std.TreeSet.Raw", "Std.TreeSet.Raw.empty"⟩,⟨"Std.ExtTreeSet", "Std.ExtTreeSet.empty"⟩,]⟩,
-    ⟨"7743a485-024d-43b6-bd5f-ebd3182eb94d", "ofList", #[⟨"Std.DHashMap", "Std.DHashMap.ofList"⟩,⟨"Std.DHashMap.Raw", "Std.DHashMap.Raw.ofList"⟩,⟨"Std.ExtDHashMap", "Std.ExtDHashMap.ofList"⟩,⟨"Std.DTreeMap", "Std.DTreeMap.ofList"⟩,⟨"Std.DTreeMap.Raw", "Std.DTreeMap.Raw.ofList"⟩,⟨"Std.ExtDTreeMap", "Std.ExtDTreeMap.ofList"⟩,⟨"Std.HashMap", "Std.HashMap.ofList"⟩,⟨"Std.HashMap.Raw", "Std.HashMap.Raw.ofList"⟩,⟨"Std.ExtHashMap", "Std.ExtHashMap.ofList"⟩,⟨"Std.TreeMap", "Std.TreeMap.ofList"⟩,⟨"Std.TreeMap.Raw", "Std.TreeMap.Raw.ofList"⟩,⟨"Std.ExtTreeMap", "Std.ExtTreeMap.ofList"⟩,⟨"Std.HashSet", "Std.HashSet.ofList"⟩,⟨"Std.HashSet.Raw", "Std.HashSet.Raw.ofList"⟩,⟨"Std.ExtHashSet", "Std.ExtHashSet.ofList"⟩,⟨"Std.TreeSet", "Std.TreeSet.ofList"⟩,⟨"Std.TreeSet.Raw", "Std.TreeSet.Raw.ofList"⟩,⟨"Std.ExtTreeSet", "Std.ExtTreeSet.ofList"⟩,]⟩,
-    ⟨"5ceaa26a-d2cb-4df3-9ac8-b5c11db2ae9d", "emptyCollection", #[⟨"Std.DHashMap", "app (EmptyCollection.emptyCollection) (Std.DHashMap*)"⟩,⟨"Std.DHashMap.Raw", "app (EmptyCollection.emptyCollection) (Std.DHashMap.Raw*)"⟩,⟨"Std.ExtDHashMap", "app (EmptyCollection.emptyCollection) (Std.ExtDHashMap*)"⟩,⟨"Std.DTreeMap", "app (EmptyCollection.emptyCollection) (Std.DTreeMap*)"⟩,⟨"Std.DTreeMap.Raw", "app (EmptyCollection.emptyCollection) (Std.DTreeMap.Raw*)"⟩,⟨"Std.ExtDTreeMap", "app (EmptyCollection.emptyCollection) (Std.ExtDTreeMap*)"⟩,⟨"Std.HashMap", "app (EmptyCollection.emptyCollection) (Std.HashMap*)"⟩,⟨"Std.HashMap.Raw", "app (EmptyCollection.emptyCollection) (Std.HashMap.Raw*)"⟩,⟨"Std.ExtHashMap", "app (EmptyCollection.emptyCollection) (Std.ExtHashMap*)"⟩,⟨"Std.TreeMap", "app (EmptyCollection.emptyCollection) (Std.TreeMap*)"⟩,⟨"Std.TreeMap.Raw", "app (EmptyCollection.emptyCollection) (Std.TreeMap.Raw*)"⟩,⟨"Std.ExtTreeMap", "app (EmptyCollection.emptyCollection) (Std.ExtTreeMap*)"⟩,⟨"Std.HashSet", "app (EmptyCollection.emptyCollection) (Std.HashSet*)"⟩,⟨"Std.HashSet.Raw", "app (EmptyCollection.emptyCollection) (Std.HashSet.Raw*)"⟩,⟨"Std.ExtHashSet", "app (EmptyCollection.emptyCollection) (Std.ExtHashSet*)"⟩,⟨"Std.TreeSet", "app (EmptyCollection.emptyCollection) (Std.TreeSet*)"⟩,⟨"Std.TreeSet.Raw", "app (EmptyCollection.emptyCollection) (Std.TreeSet.Raw*)"⟩,⟨"Std.ExtTreeSet", "app (EmptyCollection.emptyCollection) (Std.ExtTreeSet*)"⟩,]⟩,
-  ]
-  facts := #[
-    «2cb3c441-9663-4ce7-9527-0f40fc29925a»,
-    «7743a485-024d-43b6-bd5f-ebd3182eb94d»,
-    «5ceaa26a-d2cb-4df3-9ac8-b5c11db2ae9d»,
-  ]
-
-def restoreState : RestoreStateM Unit := do
-  addAssociationTable table

doc/std/grove/GroveStdlib/Generated/associative-modification-operations.lean

@@ -1,21 +0,0 @@
-import Grove.Framework
-
-/-
-This file is autogenerated by grove. You can manually edit it, for example to resolve merge
-conflicts, but be careful.
--/
-
-open Grove.Framework Widget
-
-namespace GroveStdlib.Generated.«associative-modification-operations»
-
-
-def table : AssociationTable.Data .subexpression where
-  widgetId := "associative-modification-operations"
-  rows := #[
-  ]
-  facts := #[
-  ]
-
-def restoreState : RestoreStateM Unit := do
-  addAssociationTable table

doc/std/grove/GroveStdlib/Generated/associative-query-operations.lean

@@ -1,445 +0,0 @@
-import Grove.Framework
-
-/-
-This file is autogenerated by grove. You can manually edit it, for example to resolve merge
-conflicts, but be careful.
--/
-
-open Grove.Framework Widget
-
-namespace GroveStdlib.Generated.«associative-query-operations»
-
-def «01f88623-fa5f-4380-9772-b30f2fec5c94» : AssociationTable.Fact .subexpression where
-  widgetId := "associative-query-operations"
-  factId := "01f88623-fa5f-4380-9772-b30f2fec5c94"
-  rowId := "01f88623-fa5f-4380-9772-b30f2fec5c94"
-  rowState := #[⟨"Std.DHashMap", "Std.DHashMap.isEmpty", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.DHashMap.isEmpty,
-      renderedStatement := "Std.DHashMap.isEmpty.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α}\n  (m : Std.DHashMap α β) : Bool",
-      isDeprecated := false })⟩,⟨"Std.DHashMap.Raw", "Std.DHashMap.Raw.isEmpty", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.DHashMap.Raw.isEmpty,
-      renderedStatement := "Std.DHashMap.Raw.isEmpty.{u, v} {α : Type u} {β : α → Type v} (m : Std.DHashMap.Raw α β) : Bool",
-      isDeprecated := false })⟩,⟨"Std.ExtDHashMap", "Std.ExtDHashMap.isEmpty", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.ExtDHashMap.isEmpty,
-      renderedStatement := "Std.ExtDHashMap.isEmpty.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α}\n  [EquivBEq α] [LawfulHashable α] (m : Std.ExtDHashMap α β) : Bool",
-      isDeprecated := false })⟩,⟨"Std.DTreeMap", "Std.DTreeMap.isEmpty", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.DTreeMap.isEmpty,
-      renderedStatement := "Std.DTreeMap.isEmpty.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}\n  (t : Std.DTreeMap α β cmp) : Bool",
-      isDeprecated := false })⟩,⟨"Std.DTreeMap.Raw", "Std.DTreeMap.Raw.isEmpty", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.DTreeMap.Raw.isEmpty,
-      renderedStatement := "Std.DTreeMap.Raw.isEmpty.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}\n  (t : Std.DTreeMap.Raw α β cmp) : Bool",
-      isDeprecated := false })⟩,⟨"Std.ExtDTreeMap", "Std.ExtDTreeMap.isEmpty", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.ExtDTreeMap.isEmpty,
-      renderedStatement := "Std.ExtDTreeMap.isEmpty.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}\n  (t : Std.ExtDTreeMap α β cmp) : Bool",
-      isDeprecated := false })⟩,⟨"Std.HashMap", "Std.HashMap.isEmpty", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.HashMap.isEmpty,
-      renderedStatement := "Std.HashMap.isEmpty.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α}\n  (m : Std.HashMap α β) : Bool",
-      isDeprecated := false })⟩,⟨"Std.HashMap.Raw", "Std.HashMap.Raw.isEmpty", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.HashMap.Raw.isEmpty,
-      renderedStatement := "Std.HashMap.Raw.isEmpty.{u, v} {α : Type u} {β : Type v} (m : Std.HashMap.Raw α β) : Bool",
-      isDeprecated := false })⟩,⟨"Std.ExtHashMap", "Std.ExtHashMap.isEmpty", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.ExtHashMap.isEmpty,
-      renderedStatement := "Std.ExtHashMap.isEmpty.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α]\n  [LawfulHashable α] (m : Std.ExtHashMap α β) : Bool",
-      isDeprecated := false })⟩,⟨"Std.TreeMap", "Std.TreeMap.isEmpty", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.TreeMap.isEmpty,
-      renderedStatement := "Std.TreeMap.isEmpty.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering}\n  (t : Std.TreeMap α β cmp) : Bool",
-      isDeprecated := false })⟩,⟨"Std.TreeMap.Raw", "Std.TreeMap.Raw.isEmpty", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.TreeMap.Raw.isEmpty,
-      renderedStatement := "Std.TreeMap.Raw.isEmpty.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering}\n  (t : Std.TreeMap.Raw α β cmp) : Bool",
-      isDeprecated := false })⟩,⟨"Std.ExtTreeMap", "Std.ExtTreeMap.isEmpty", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.ExtTreeMap.isEmpty,
-      renderedStatement := "Std.ExtTreeMap.isEmpty.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering}\n  (t : Std.ExtTreeMap α β cmp) : Bool",
-      isDeprecated := false })⟩,⟨"Std.HashSet", "Std.HashSet.isEmpty", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.HashSet.isEmpty,
-      renderedStatement := "Std.HashSet.isEmpty.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} (m : Std.HashSet α) : Bool",
-      isDeprecated := false })⟩,⟨"Std.HashSet.Raw", "Std.HashSet.Raw.isEmpty", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.HashSet.Raw.isEmpty,
-      renderedStatement := "Std.HashSet.Raw.isEmpty.{u} {α : Type u} (m : Std.HashSet.Raw α) : Bool",
-      isDeprecated := false })⟩,⟨"Std.ExtHashSet", "Std.ExtHashSet.isEmpty", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.ExtHashSet.isEmpty,
-      renderedStatement := "Std.ExtHashSet.isEmpty.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α]\n  [LawfulHashable α] (m : Std.ExtHashSet α) : Bool",
-      isDeprecated := false })⟩,⟨"Std.TreeSet", "Std.TreeSet.isEmpty", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.TreeSet.isEmpty,
-      renderedStatement := "Std.TreeSet.isEmpty.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.TreeSet α cmp) : Bool",
-      isDeprecated := false })⟩,⟨"Std.TreeSet.Raw", "Std.TreeSet.Raw.isEmpty", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.TreeSet.Raw.isEmpty,
-      renderedStatement := "Std.TreeSet.Raw.isEmpty.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.TreeSet.Raw α cmp) : Bool",
-      isDeprecated := false })⟩,⟨"Std.ExtTreeSet", "Std.ExtTreeSet.isEmpty", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.ExtTreeSet.isEmpty,
-      renderedStatement := "Std.ExtTreeSet.isEmpty.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.ExtTreeSet α cmp) : Bool",
-      isDeprecated := false })⟩,]
-  metadata := {
-    status := .done
-    comment := ""
-  }
-def «f084f852-af71-45b6-8ab3-d251a8144f72» : AssociationTable.Fact .subexpression where
-  widgetId := "associative-query-operations"
-  factId := "f084f852-af71-45b6-8ab3-d251a8144f72"
-  rowId := "f084f852-af71-45b6-8ab3-d251a8144f72"
-  rowState := #[⟨"Std.DHashMap", "Std.DHashMap.size", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.DHashMap.size,
-      renderedStatement := "Std.DHashMap.size.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α}\n  (m : Std.DHashMap α β) : Nat",
-      isDeprecated := false })⟩,⟨"Std.DHashMap.Raw", "Std.DHashMap.Raw.size", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.DHashMap.Raw.size,
-      renderedStatement := "Std.DHashMap.Raw.size.{u, v} {α : Type u} {β : α → Type v} (self : Std.DHashMap.Raw α β) : Nat",
-      isDeprecated := false })⟩,⟨"Std.ExtDHashMap", "Std.ExtDHashMap.size", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.ExtDHashMap.size,
-      renderedStatement := "Std.ExtDHashMap.size.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α}\n  [EquivBEq α] [LawfulHashable α] (m : Std.ExtDHashMap α β) : Nat",
-      isDeprecated := false })⟩,⟨"Std.DTreeMap", "Std.DTreeMap.size", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.DTreeMap.size,
-      renderedStatement := "Std.DTreeMap.size.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}\n  (t : Std.DTreeMap α β cmp) : Nat",
-      isDeprecated := false })⟩,⟨"Std.DTreeMap.Raw", "Std.DTreeMap.Raw.size", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.DTreeMap.Raw.size,
-      renderedStatement := "Std.DTreeMap.Raw.size.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}\n  (t : Std.DTreeMap.Raw α β cmp) : Nat",
-      isDeprecated := false })⟩,⟨"Std.ExtDTreeMap", "Std.ExtDTreeMap.size", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.ExtDTreeMap.size,
-      renderedStatement := "Std.ExtDTreeMap.size.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}\n  (t : Std.ExtDTreeMap α β cmp) : Nat",
-      isDeprecated := false })⟩,⟨"Std.HashMap", "Std.HashMap.size", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.HashMap.size,
-      renderedStatement := "Std.HashMap.size.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α}\n  (m : Std.HashMap α β) : Nat",
-      isDeprecated := false })⟩,⟨"Std.HashMap.Raw", "Std.HashMap.Raw.size", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.HashMap.Raw.size,
-      renderedStatement := "Std.HashMap.Raw.size.{u, v} {α : Type u} {β : Type v} (m : Std.HashMap.Raw α β) : Nat",
-      isDeprecated := false })⟩,⟨"Std.ExtHashMap", "Std.ExtHashMap.size", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.ExtHashMap.size,
-      renderedStatement := "Std.ExtHashMap.size.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α]\n  [LawfulHashable α] (m : Std.ExtHashMap α β) : Nat",
-      isDeprecated := false })⟩,⟨"Std.TreeMap", "Std.TreeMap.size", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.TreeMap.size,
-      renderedStatement := "Std.TreeMap.size.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering}\n  (t : Std.TreeMap α β cmp) : Nat",
-      isDeprecated := false })⟩,⟨"Std.TreeMap.Raw", "Std.TreeMap.Raw.size", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.TreeMap.Raw.size,
-      renderedStatement := "Std.TreeMap.Raw.size.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering}\n  (t : Std.TreeMap.Raw α β cmp) : Nat",
-      isDeprecated := false })⟩,⟨"Std.ExtTreeMap", "Std.ExtTreeMap.size", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.ExtTreeMap.size,
-      renderedStatement := "Std.ExtTreeMap.size.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering}\n  (t : Std.ExtTreeMap α β cmp) : Nat",
-      isDeprecated := false })⟩,⟨"Std.HashSet", "Std.HashSet.size", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.HashSet.size,
-      renderedStatement := "Std.HashSet.size.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} (m : Std.HashSet α) : Nat",
-      isDeprecated := false })⟩,⟨"Std.HashSet.Raw", "Std.HashSet.Raw.size", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.HashSet.Raw.size,
-      renderedStatement := "Std.HashSet.Raw.size.{u} {α : Type u} (m : Std.HashSet.Raw α) : Nat",
-      isDeprecated := false })⟩,⟨"Std.ExtHashSet", "Std.ExtHashSet.size", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.ExtHashSet.size,
-      renderedStatement := "Std.ExtHashSet.size.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α]\n  (m : Std.ExtHashSet α) : Nat",
-      isDeprecated := false })⟩,⟨"Std.TreeSet", "Std.TreeSet.size", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.TreeSet.size,
-      renderedStatement := "Std.TreeSet.size.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.TreeSet α cmp) : Nat",
-      isDeprecated := false })⟩,⟨"Std.TreeSet.Raw", "Std.TreeSet.Raw.size", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.TreeSet.Raw.size,
-      renderedStatement := "Std.TreeSet.Raw.size.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.TreeSet.Raw α cmp) : Nat",
-      isDeprecated := false })⟩,⟨"Std.ExtTreeSet", "Std.ExtTreeSet.size", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.ExtTreeSet.size,
-      renderedStatement := "Std.ExtTreeSet.size.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.ExtTreeSet α cmp) : Nat",
-      isDeprecated := false })⟩,]
-  metadata := {
-    status := .done
-    comment := ""
-  }
-def «f4e6fa70-5aed-439d-aaad-5f4ced65bf7b» : AssociationTable.Fact .subexpression where
-  widgetId := "associative-query-operations"
-  factId := "f4e6fa70-5aed-439d-aaad-5f4ced65bf7b"
-  rowId := "f4e6fa70-5aed-439d-aaad-5f4ced65bf7b"
-  rowState := #[⟨"Std.DTreeMap", "Std.DTreeMap.any", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.DTreeMap.any,
-      renderedStatement := "Std.DTreeMap.any.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}\n  (t : Std.DTreeMap α β cmp) (p : (a : α) → β a → Bool) : Bool",
-      isDeprecated := false })⟩,⟨"Std.DTreeMap.Raw", "Std.DTreeMap.Raw.any", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.DTreeMap.Raw.any,
-      renderedStatement := "Std.DTreeMap.Raw.any.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}\n  (t : Std.DTreeMap.Raw α β cmp) (p : (a : α) → β a → Bool) : Bool",
-      isDeprecated := false })⟩,⟨"Std.ExtDTreeMap", "Std.ExtDTreeMap.any", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.ExtDTreeMap.any,
-      renderedStatement := "Std.ExtDTreeMap.any.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp]\n  (t : Std.ExtDTreeMap α β cmp) (p : (a : α) → β a → Bool) : Bool",
-      isDeprecated := false })⟩,⟨"Std.TreeMap", "Std.TreeMap.any", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.TreeMap.any,
-      renderedStatement := "Std.TreeMap.any.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp)\n  (p : α → β → Bool) : Bool",
-      isDeprecated := false })⟩,⟨"Std.TreeMap.Raw", "Std.TreeMap.Raw.any", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.TreeMap.Raw.any,
-      renderedStatement := "Std.TreeMap.Raw.any.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering}\n  (t : Std.TreeMap.Raw α β cmp) (p : α → β → Bool) : Bool",
-      isDeprecated := false })⟩,⟨"Std.ExtTreeMap", "Std.ExtTreeMap.any", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.ExtTreeMap.any,
-      renderedStatement := "Std.ExtTreeMap.any.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp]\n  (t : Std.ExtTreeMap α β cmp) (p : α → β → Bool) : Bool",
-      isDeprecated := false })⟩,⟨"Std.HashSet", "Std.HashSet.any", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.HashSet.any,
-      renderedStatement := "Std.HashSet.any.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} (m : Std.HashSet α)\n  (p : α → Bool) : Bool",
-      isDeprecated := false })⟩,⟨"Std.HashSet.Raw", "Std.HashSet.Raw.any", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.HashSet.Raw.any,
-      renderedStatement := "Std.HashSet.Raw.any.{u} {α : Type u} (m : Std.HashSet.Raw α) (p : α → Bool) : Bool",
-      isDeprecated := false })⟩,⟨"Std.TreeSet", "Std.TreeSet.any", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.TreeSet.any,
-      renderedStatement := "Std.TreeSet.any.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.TreeSet α cmp) (p : α → Bool) :\n  Bool",
-      isDeprecated := false })⟩,⟨"Std.TreeSet.Raw", "Std.TreeSet.Raw.any", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.TreeSet.Raw.any,
-      renderedStatement := "Std.TreeSet.Raw.any.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.TreeSet.Raw α cmp)\n  (p : α → Bool) : Bool",
-      isDeprecated := false })⟩,⟨"Std.ExtTreeSet", "Std.ExtTreeSet.any", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.ExtTreeSet.any,
-      renderedStatement := "Std.ExtTreeSet.any.{u} {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp]\n  (t : Std.ExtTreeSet α cmp) (p : α → Bool) : Bool",
-      isDeprecated := false })⟩,]
-  metadata := {
-    status := .bad
-    comment := "Missing for some containers"
-  }
-def «c1d181f6-3204-4956-946f-e81619f9feb4» : AssociationTable.Fact .subexpression where
-  widgetId := "associative-query-operations"
-  factId := "c1d181f6-3204-4956-946f-e81619f9feb4"
-  rowId := "c1d181f6-3204-4956-946f-e81619f9feb4"
-  rowState := #[⟨"Std.DTreeMap", "Std.DTreeMap.all", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.DTreeMap.all,
-      renderedStatement := "Std.DTreeMap.all.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}\n  (t : Std.DTreeMap α β cmp) (p : (a : α) → β a → Bool) : Bool",
-      isDeprecated := false })⟩,⟨"Std.DTreeMap.Raw", "Std.DTreeMap.Raw.all", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.DTreeMap.Raw.all,
-      renderedStatement := "Std.DTreeMap.Raw.all.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}\n  (t : Std.DTreeMap.Raw α β cmp) (p : (a : α) → β a → Bool) : Bool",
-      isDeprecated := false })⟩,⟨"Std.ExtDTreeMap", "Std.ExtDTreeMap.all", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.ExtDTreeMap.all,
-      renderedStatement := "Std.ExtDTreeMap.all.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp]\n  (t : Std.ExtDTreeMap α β cmp) (p : (a : α) → β a → Bool) : Bool",
-      isDeprecated := false })⟩,⟨"Std.TreeMap", "Std.TreeMap.all", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.TreeMap.all,
-      renderedStatement := "Std.TreeMap.all.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp)\n  (p : α → β → Bool) : Bool",
-      isDeprecated := false })⟩,⟨"Std.TreeMap.Raw", "Std.TreeMap.Raw.all", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.TreeMap.Raw.all,
-      renderedStatement := "Std.TreeMap.Raw.all.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering}\n  (t : Std.TreeMap.Raw α β cmp) (p : α → β → Bool) : Bool",
-      isDeprecated := false })⟩,⟨"Std.ExtTreeMap", "Std.ExtTreeMap.all", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.ExtTreeMap.all,
-      renderedStatement := "Std.ExtTreeMap.all.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp]\n  (t : Std.ExtTreeMap α β cmp) (p : α → β → Bool) : Bool",
-      isDeprecated := false })⟩,⟨"Std.HashSet", "Std.HashSet.all", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.HashSet.all,
-      renderedStatement := "Std.HashSet.all.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} (m : Std.HashSet α)\n  (p : α → Bool) : Bool",
-      isDeprecated := false })⟩,⟨"Std.HashSet.Raw", "Std.HashSet.Raw.all", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.HashSet.Raw.all,
-      renderedStatement := "Std.HashSet.Raw.all.{u} {α : Type u} (m : Std.HashSet.Raw α) (p : α → Bool) : Bool",
-      isDeprecated := false })⟩,⟨"Std.TreeSet", "Std.TreeSet.all", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.TreeSet.all,
-      renderedStatement := "Std.TreeSet.all.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.TreeSet α cmp) (p : α → Bool) :\n  Bool",
-      isDeprecated := false })⟩,⟨"Std.TreeSet.Raw", "Std.TreeSet.Raw.all", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.TreeSet.Raw.all,
-      renderedStatement := "Std.TreeSet.Raw.all.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.TreeSet.Raw α cmp)\n  (p : α → Bool) : Bool",
-      isDeprecated := false })⟩,⟨"Std.ExtTreeSet", "Std.ExtTreeSet.all", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.ExtTreeSet.all,
-      renderedStatement := "Std.ExtTreeSet.all.{u} {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp]\n  (t : Std.ExtTreeSet α cmp) (p : α → Bool) : Bool",
-      isDeprecated := false })⟩,]
-  metadata := {
-    status := .bad
-    comment := "Missing for some containers"
-  }
-def «efe57f41-7db7-4303-b3a6-5216a70c43ce» : AssociationTable.Fact .subexpression where
-  widgetId := "associative-query-operations"
-  factId := "efe57f41-7db7-4303-b3a6-5216a70c43ce"
-  rowId := "efe57f41-7db7-4303-b3a6-5216a70c43ce"
-  rowState := #[⟨"Std.DHashMap", "Std.DHashMap.getD", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.DHashMap.getD,
-      renderedStatement := "Std.DHashMap.getD.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [LawfulBEq α]\n  (m : Std.DHashMap α β) (a : α) (fallback : β a) : β a",
-      isDeprecated := false })⟩,⟨"Std.DHashMap.Raw", "Std.DHashMap.Raw.getD", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.DHashMap.Raw.getD,
-      renderedStatement := "Std.DHashMap.Raw.getD.{u, v} {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α]\n  (m : Std.DHashMap.Raw α β) (a : α) (fallback : β a) : β a",
-      isDeprecated := false })⟩,⟨"Std.ExtDHashMap", "Std.ExtDHashMap.getD", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.ExtDHashMap.getD,
-      renderedStatement := "Std.ExtDHashMap.getD.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α}\n  [LawfulBEq α] (m : Std.ExtDHashMap α β) (a : α) (fallback : β a) : β a",
-      isDeprecated := false })⟩,⟨"Std.DTreeMap", "Std.DTreeMap.getD", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.DTreeMap.getD,
-      renderedStatement := "Std.DTreeMap.getD.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}\n  [Std.LawfulEqCmp cmp] (t : Std.DTreeMap α β cmp) (a : α) (fallback : β a) : β a",
-      isDeprecated := false })⟩,⟨"Std.DTreeMap.Raw", "Std.DTreeMap.Raw.getD", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.DTreeMap.Raw.getD,
-      renderedStatement := "Std.DTreeMap.Raw.getD.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}\n  [Std.LawfulEqCmp cmp] (t : Std.DTreeMap.Raw α β cmp) (a : α) (fallback : β a) : β a",
-      isDeprecated := false })⟩,⟨"Std.ExtDTreeMap", "Std.ExtDTreeMap.getD", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.ExtDTreeMap.getD,
-      renderedStatement := "Std.ExtDTreeMap.getD.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}\n  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] (t : Std.ExtDTreeMap α β cmp) (a : α) (fallback : β a) :\n  β a",
-      isDeprecated := false })⟩,⟨"Std.HashMap", "Std.HashMap.getD", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.HashMap.getD,
-      renderedStatement := "Std.HashMap.getD.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α}\n  (m : Std.HashMap α β) (a : α) (fallback : β) : β",
-      isDeprecated := false })⟩,⟨"Std.HashMap.Raw", "Std.HashMap.Raw.getD", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.HashMap.Raw.getD,
-      renderedStatement := "Std.HashMap.Raw.getD.{u, v} {α : Type u} {β : Type v} [BEq α] [Hashable α] (m : Std.HashMap.Raw α β)\n  (a : α) (fallback : β) : β",
-      isDeprecated := false })⟩,⟨"Std.ExtHashMap", "Std.ExtHashMap.getD", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.ExtHashMap.getD,
-      renderedStatement := "Std.ExtHashMap.getD.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α]\n  [LawfulHashable α] (m : Std.ExtHashMap α β) (a : α) (fallback : β) : β",
-      isDeprecated := false })⟩,⟨"Std.TreeMap", "Std.TreeMap.getD", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.TreeMap.getD,
-      renderedStatement := "Std.TreeMap.getD.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp)\n  (a : α) (fallback : β) : β",
-      isDeprecated := false })⟩,⟨"Std.TreeMap.Raw", "Std.TreeMap.Raw.getD", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.TreeMap.Raw.getD,
-      renderedStatement := "Std.TreeMap.Raw.getD.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering}\n  (t : Std.TreeMap.Raw α β cmp) (a : α) (fallback : β) : β",
-      isDeprecated := false })⟩,⟨"Std.ExtTreeMap", "Std.ExtTreeMap.getD", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.ExtTreeMap.getD,
-      renderedStatement := "Std.ExtTreeMap.getD.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp]\n  (t : Std.ExtTreeMap α β cmp) (a : α) (fallback : β) : β",
-      isDeprecated := false })⟩,⟨"Std.HashSet", "Std.HashSet.getD", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.HashSet.getD,
-      renderedStatement := "Std.HashSet.getD.{u} {α : Type u} [BEq α] [Hashable α] (m : Std.HashSet α) (a fallback : α) : α",
-      isDeprecated := false })⟩,⟨"Std.HashSet.Raw", "Std.HashSet.Raw.getD", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.HashSet.Raw.getD,
-      renderedStatement := "Std.HashSet.Raw.getD.{u} {α : Type u} [BEq α] [Hashable α] (m : Std.HashSet.Raw α)\n  (a fallback : α) : α",
-      isDeprecated := false })⟩,⟨"Std.ExtHashSet", "Std.ExtHashSet.getD", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.ExtHashSet.getD,
-      renderedStatement := "Std.ExtHashSet.getD.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α]\n  (m : Std.ExtHashSet α) (a fallback : α) : α",
-      isDeprecated := false })⟩,⟨"Std.TreeSet", "Std.TreeSet.getD", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.TreeSet.getD,
-      renderedStatement := "Std.TreeSet.getD.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.TreeSet α cmp)\n  (a fallback : α) : α",
-      isDeprecated := false })⟩,⟨"Std.TreeSet.Raw", "Std.TreeSet.Raw.getD", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.TreeSet.Raw.getD,
-      renderedStatement := "Std.TreeSet.Raw.getD.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.TreeSet.Raw α cmp)\n  (a fallback : α) : α",
-      isDeprecated := false })⟩,⟨"Std.ExtTreeSet", "Std.ExtTreeSet.getD", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.ExtTreeSet.getD,
-      renderedStatement := "Std.ExtTreeSet.getD.{u} {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp]\n  (t : Std.ExtTreeSet α cmp) (a fallback : α) : α",
-      isDeprecated := false })⟩,]
-  metadata := {
-    status := .done
-    comment := ""
-  }
-def «e23b1119-3b57-433e-a68d-68fd70b9943d» : AssociationTable.Fact .subexpression where
-  widgetId := "associative-query-operations"
-  factId := "e23b1119-3b57-433e-a68d-68fd70b9943d"
-  rowId := "e23b1119-3b57-433e-a68d-68fd70b9943d"
-  rowState := #[⟨"Std.DHashMap", "Std.DHashMap.get", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.DHashMap.get,
-      renderedStatement := "Std.DHashMap.get.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [LawfulBEq α]\n  (m : Std.DHashMap α β) (a : α) (h : a ∈ m) : β a",
-      isDeprecated := false })⟩,⟨"Std.DHashMap.Raw", "Std.DHashMap.Raw.Const.get", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.DHashMap.Raw.Const.get,
-      renderedStatement := "Std.DHashMap.Raw.Const.get.{u, v} {α : Type u} {β : Type v} [BEq α] [Hashable α]\n  (m : Std.DHashMap.Raw α fun x => β) (a : α) (h : a ∈ m) : β",
-      isDeprecated := false })⟩,⟨"Std.ExtDHashMap", "Std.ExtDHashMap.get", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.ExtDHashMap.get,
-      renderedStatement := "Std.ExtDHashMap.get.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α}\n  [LawfulBEq α] (m : Std.ExtDHashMap α β) (a : α) (h : a ∈ m) : β a",
-      isDeprecated := false })⟩,⟨"Std.DTreeMap", "Std.DTreeMap.get", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.DTreeMap.get,
-      renderedStatement := "Std.DTreeMap.get.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.LawfulEqCmp cmp]\n  (t : Std.DTreeMap α β cmp) (a : α) (h : a ∈ t) : β a",
-      isDeprecated := false })⟩,⟨"Std.DTreeMap.Raw", "Std.DTreeMap.Raw.get", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.DTreeMap.Raw.get,
-      renderedStatement := "Std.DTreeMap.Raw.get.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}\n  [Std.LawfulEqCmp cmp] (t : Std.DTreeMap.Raw α β cmp) (a : α) (h : a ∈ t) : β a",
-      isDeprecated := false })⟩,⟨"Std.ExtDTreeMap", "Std.ExtDTreeMap.get", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.ExtDTreeMap.get,
-      renderedStatement := "Std.ExtDTreeMap.get.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp]\n  [Std.LawfulEqCmp cmp] (t : Std.ExtDTreeMap α β cmp) (a : α) (h : a ∈ t) : β a",
-      isDeprecated := false })⟩,⟨"Std.HashMap", "app (GetElem.getElem) (Std.HashMap*)", Grove.Framework.Subexpression.State.predicate
-  { key := "app (GetElem.getElem) (Std.HashMap*)", displayShort := "Std.HashMap[·]" }⟩,⟨"Std.HashMap.Raw", "app (GetElem.getElem) (Std.HashMap.Raw*)", Grove.Framework.Subexpression.State.predicate
-  { key := "app (GetElem.getElem) (Std.HashMap.Raw*)", displayShort := "Std.HashMap.Raw[·]" }⟩,⟨"Std.ExtHashMap", "app (GetElem.getElem) (Std.ExtHashMap*)", Grove.Framework.Subexpression.State.predicate
-  { key := "app (GetElem.getElem) (Std.ExtHashMap*)", displayShort := "Std.ExtHashMap[·]" }⟩,⟨"Std.TreeMap", "app (GetElem.getElem) (Std.TreeMap*)", Grove.Framework.Subexpression.State.predicate
-  { key := "app (GetElem.getElem) (Std.TreeMap*)", displayShort := "Std.TreeMap[·]" }⟩,⟨"Std.TreeMap.Raw", "app (GetElem.getElem) (Std.TreeMap.Raw*)", Grove.Framework.Subexpression.State.predicate
-  { key := "app (GetElem.getElem) (Std.TreeMap.Raw*)", displayShort := "Std.TreeMap.Raw[·]" }⟩,⟨"Std.ExtTreeMap", "app (GetElem.getElem) (Std.ExtTreeMap*)", Grove.Framework.Subexpression.State.predicate
-  { key := "app (GetElem.getElem) (Std.ExtTreeMap*)", displayShort := "Std.ExtTreeMap[·]" }⟩,⟨"Std.HashSet", "Std.HashSet.get", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.HashSet.get,
-      renderedStatement := "Std.HashSet.get.{u} {α : Type u} [BEq α] [Hashable α] (m : Std.HashSet α) (a : α) (h : a ∈ m) : α",
-      isDeprecated := false })⟩,⟨"Std.HashSet.Raw", "Std.HashSet.Raw.get", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.HashSet.Raw.get,
-      renderedStatement := "Std.HashSet.Raw.get.{u} {α : Type u} [BEq α] [Hashable α] (m : Std.HashSet.Raw α) (a : α)\n  (h : a ∈ m) : α",
-      isDeprecated := false })⟩,⟨"Std.ExtHashSet", "Std.ExtHashSet.get", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.ExtHashSet.get,
-      renderedStatement := "Std.ExtHashSet.get.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α]\n  (m : Std.ExtHashSet α) (a : α) (h : a ∈ m) : α",
-      isDeprecated := false })⟩,⟨"Std.TreeSet", "Std.TreeSet.get", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.TreeSet.get,
-      renderedStatement := "Std.TreeSet.get.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.TreeSet α cmp) (a : α)\n  (h : a ∈ t) : α",
-      isDeprecated := false })⟩,⟨"Std.TreeSet.Raw", "Std.TreeSet.Raw.get", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.TreeSet.Raw.get,
-      renderedStatement := "Std.TreeSet.Raw.get.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.TreeSet.Raw α cmp) (a : α)\n  (h : a ∈ t) : α",
-      isDeprecated := false })⟩,⟨"Std.ExtTreeSet", "Std.ExtTreeSet.get", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.ExtTreeSet.get,
-      renderedStatement := "Std.ExtTreeSet.get.{u} {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp]\n  (t : Std.ExtTreeSet α cmp) (a : α) (h : a ∈ t) : α",
-      isDeprecated := false })⟩,]
-  metadata := {
-    status := .bad
-    comment := "Should *Set have GetElem?"
-  }
-
-def table : AssociationTable.Data .subexpression where
-  widgetId := "associative-query-operations"
-  rows := #[
-    ⟨"01f88623-fa5f-4380-9772-b30f2fec5c94", "isEmpty", #[⟨"Std.DHashMap", "Std.DHashMap.isEmpty"⟩,⟨"Std.DHashMap.Raw", "Std.DHashMap.Raw.isEmpty"⟩,⟨"Std.ExtDHashMap", "Std.ExtDHashMap.isEmpty"⟩,⟨"Std.DTreeMap", "Std.DTreeMap.isEmpty"⟩,⟨"Std.DTreeMap.Raw", "Std.DTreeMap.Raw.isEmpty"⟩,⟨"Std.ExtDTreeMap", "Std.ExtDTreeMap.isEmpty"⟩,⟨"Std.HashMap", "Std.HashMap.isEmpty"⟩,⟨"Std.HashMap.Raw", "Std.HashMap.Raw.isEmpty"⟩,⟨"Std.ExtHashMap", "Std.ExtHashMap.isEmpty"⟩,⟨"Std.TreeMap", "Std.TreeMap.isEmpty"⟩,⟨"Std.TreeMap.Raw", "Std.TreeMap.Raw.isEmpty"⟩,⟨"Std.ExtTreeMap", "Std.ExtTreeMap.isEmpty"⟩,⟨"Std.HashSet", "Std.HashSet.isEmpty"⟩,⟨"Std.HashSet.Raw", "Std.HashSet.Raw.isEmpty"⟩,⟨"Std.ExtHashSet", "Std.ExtHashSet.isEmpty"⟩,⟨"Std.TreeSet", "Std.TreeSet.isEmpty"⟩,⟨"Std.TreeSet.Raw", "Std.TreeSet.Raw.isEmpty"⟩,⟨"Std.ExtTreeSet", "Std.ExtTreeSet.isEmpty"⟩,]⟩,
-    ⟨"f084f852-af71-45b6-8ab3-d251a8144f72", "size", #[⟨"Std.DHashMap", "Std.DHashMap.size"⟩,⟨"Std.DHashMap.Raw", "Std.DHashMap.Raw.size"⟩,⟨"Std.ExtDHashMap", "Std.ExtDHashMap.size"⟩,⟨"Std.DTreeMap", "Std.DTreeMap.size"⟩,⟨"Std.DTreeMap.Raw", "Std.DTreeMap.Raw.size"⟩,⟨"Std.ExtDTreeMap", "Std.ExtDTreeMap.size"⟩,⟨"Std.HashMap", "Std.HashMap.size"⟩,⟨"Std.HashMap.Raw", "Std.HashMap.Raw.size"⟩,⟨"Std.ExtHashMap", "Std.ExtHashMap.size"⟩,⟨"Std.TreeMap", "Std.TreeMap.size"⟩,⟨"Std.TreeMap.Raw", "Std.TreeMap.Raw.size"⟩,⟨"Std.ExtTreeMap", "Std.ExtTreeMap.size"⟩,⟨"Std.HashSet", "Std.HashSet.size"⟩,⟨"Std.HashSet.Raw", "Std.HashSet.Raw.size"⟩,⟨"Std.ExtHashSet", "Std.ExtHashSet.size"⟩,⟨"Std.TreeSet", "Std.TreeSet.size"⟩,⟨"Std.TreeSet.Raw", "Std.TreeSet.Raw.size"⟩,⟨"Std.ExtTreeSet", "Std.ExtTreeSet.size"⟩,]⟩,
-    ⟨"f4e6fa70-5aed-439d-aaad-5f4ced65bf7b", "any", #[⟨"Std.DTreeMap", "Std.DTreeMap.any"⟩,⟨"Std.DTreeMap.Raw", "Std.DTreeMap.Raw.any"⟩,⟨"Std.ExtDTreeMap", "Std.ExtDTreeMap.any"⟩,⟨"Std.TreeMap", "Std.TreeMap.any"⟩,⟨"Std.TreeMap.Raw", "Std.TreeMap.Raw.any"⟩,⟨"Std.ExtTreeMap", "Std.ExtTreeMap.any"⟩,⟨"Std.HashSet", "Std.HashSet.any"⟩,⟨"Std.HashSet.Raw", "Std.HashSet.Raw.any"⟩,⟨"Std.TreeSet", "Std.TreeSet.any"⟩,⟨"Std.TreeSet.Raw", "Std.TreeSet.Raw.any"⟩,⟨"Std.ExtTreeSet", "Std.ExtTreeSet.any"⟩,]⟩,
-    ⟨"c1d181f6-3204-4956-946f-e81619f9feb4", "all", #[⟨"Std.DTreeMap", "Std.DTreeMap.all"⟩,⟨"Std.DTreeMap.Raw", "Std.DTreeMap.Raw.all"⟩,⟨"Std.ExtDTreeMap", "Std.ExtDTreeMap.all"⟩,⟨"Std.TreeMap", "Std.TreeMap.all"⟩,⟨"Std.TreeMap.Raw", "Std.TreeMap.Raw.all"⟩,⟨"Std.ExtTreeMap", "Std.ExtTreeMap.all"⟩,⟨"Std.HashSet", "Std.HashSet.all"⟩,⟨"Std.HashSet.Raw", "Std.HashSet.Raw.all"⟩,⟨"Std.TreeSet", "Std.TreeSet.all"⟩,⟨"Std.TreeSet.Raw", "Std.TreeSet.Raw.all"⟩,⟨"Std.ExtTreeSet", "Std.ExtTreeSet.all"⟩,]⟩,
-    ⟨"efe57f41-7db7-4303-b3a6-5216a70c43ce", "getD", #[⟨"Std.DHashMap", "Std.DHashMap.getD"⟩,⟨"Std.DHashMap.Raw", "Std.DHashMap.Raw.getD"⟩,⟨"Std.ExtDHashMap", "Std.ExtDHashMap.getD"⟩,⟨"Std.DTreeMap", "Std.DTreeMap.getD"⟩,⟨"Std.DTreeMap.Raw", "Std.DTreeMap.Raw.getD"⟩,⟨"Std.ExtDTreeMap", "Std.ExtDTreeMap.getD"⟩,⟨"Std.HashMap", "Std.HashMap.getD"⟩,⟨"Std.HashMap.Raw", "Std.HashMap.Raw.getD"⟩,⟨"Std.ExtHashMap", "Std.ExtHashMap.getD"⟩,⟨"Std.TreeMap", "Std.TreeMap.getD"⟩,⟨"Std.TreeMap.Raw", "Std.TreeMap.Raw.getD"⟩,⟨"Std.ExtTreeMap", "Std.ExtTreeMap.getD"⟩,⟨"Std.HashSet", "Std.HashSet.getD"⟩,⟨"Std.HashSet.Raw", "Std.HashSet.Raw.getD"⟩,⟨"Std.ExtHashSet", "Std.ExtHashSet.getD"⟩,⟨"Std.TreeSet", "Std.TreeSet.getD"⟩,⟨"Std.TreeSet.Raw", "Std.TreeSet.Raw.getD"⟩,⟨"Std.ExtTreeSet", "Std.ExtTreeSet.getD"⟩,]⟩,
-    ⟨"e23b1119-3b57-433e-a68d-68fd70b9943d", "getElem", #[⟨"Std.DHashMap", "Std.DHashMap.get"⟩,⟨"Std.DHashMap.Raw", "Std.DHashMap.Raw.Const.get"⟩,⟨"Std.ExtDHashMap", "Std.ExtDHashMap.get"⟩,⟨"Std.DTreeMap", "Std.DTreeMap.get"⟩,⟨"Std.DTreeMap.Raw", "Std.DTreeMap.Raw.get"⟩,⟨"Std.ExtDTreeMap", "Std.ExtDTreeMap.get"⟩,⟨"Std.HashMap", "app (GetElem.getElem) (Std.HashMap*)"⟩,⟨"Std.HashMap.Raw", "app (GetElem.getElem) (Std.HashMap.Raw*)"⟩,⟨"Std.ExtHashMap", "app (GetElem.getElem) (Std.ExtHashMap*)"⟩,⟨"Std.TreeMap", "app (GetElem.getElem) (Std.TreeMap*)"⟩,⟨"Std.TreeMap.Raw", "app (GetElem.getElem) (Std.TreeMap.Raw*)"⟩,⟨"Std.ExtTreeMap", "app (GetElem.getElem) (Std.ExtTreeMap*)"⟩,⟨"Std.HashSet", "Std.HashSet.get"⟩,⟨"Std.HashSet.Raw", "Std.HashSet.Raw.get"⟩,⟨"Std.ExtHashSet", "Std.ExtHashSet.get"⟩,⟨"Std.TreeSet", "Std.TreeSet.get"⟩,⟨"Std.TreeSet.Raw", "Std.TreeSet.Raw.get"⟩,⟨"Std.ExtTreeSet", "Std.ExtTreeSet.get"⟩,]⟩,
-  ]
-  facts := #[
-    «01f88623-fa5f-4380-9772-b30f2fec5c94»,
-    «f084f852-af71-45b6-8ab3-d251a8144f72»,
-    «f4e6fa70-5aed-439d-aaad-5f4ced65bf7b»,
-    «c1d181f6-3204-4956-946f-e81619f9feb4»,
-    «efe57f41-7db7-4303-b3a6-5216a70c43ce»,
-    «e23b1119-3b57-433e-a68d-68fd70b9943d»,
-  ]
-
-def restoreState : RestoreStateM Unit := do
-  addAssociationTable table

doc/std/grove/GroveStdlib/Std.lean

@@ -1,31 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel
--/
-import GroveStdlib.Std.CoreTypesAndOperations
-import GroveStdlib.Std.LanguageConstructs
-import GroveStdlib.Std.Libraries
-import GroveStdlib.Std.OperatingSystemAbstractions
-
-open Grove.Framework Widget
-
-namespace GroveStdlib
-
-namespace Std
-
-def introduction : Node :=
-  .text "Welcome to the interactive Lean standard library outline!"
-
-end Std
-
-def std : Node :=
-  .section "stdlib" "The Lean standard library" #[
-    Std.introduction,
-    Std.coreTypesAndOperations,
-    Std.languageConstructs,
-    Std.libraries,
-    Std.operatingSystemAbstractions
-  ]
-
-end GroveStdlib

doc/std/grove/GroveStdlib/Std/CoreTypesAndOperations.lean

@@ -1,28 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel
--/
-import Grove.Framework
-import GroveStdlib.Std.CoreTypesAndOperations.BasicTypes
-import GroveStdlib.Std.CoreTypesAndOperations.Containers
-import GroveStdlib.Std.CoreTypesAndOperations.Numbers
-import GroveStdlib.Std.CoreTypesAndOperations.StringsAndFormatting
-
-open Grove.Framework Widget
-
-namespace GroveStdlib.Std
-
-namespace CoreTypesAndOperations
-
-end CoreTypesAndOperations
-
-def coreTypesAndOperations : Node :=
-  .section "core-types-and-operations" "Core types and operations" #[
-    CoreTypesAndOperations.basicTypes,
-    CoreTypesAndOperations.containers,
-    CoreTypesAndOperations.numbers,
-    CoreTypesAndOperations.stringsAndFormatting
-  ]
-
-end GroveStdlib.Std

doc/std/grove/GroveStdlib/Std/CoreTypesAndOperations/BasicTypes.lean

@@ -1,19 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel
--/
-import Grove.Framework
-
-open Grove.Framework Widget
-
-namespace GroveStdlib.Std.CoreTypesAndOperations
-
-namespace BasicTypes
-
-end BasicTypes
-
-def basicTypes : Node :=
-  .section "basic-types" "Basic types" #[]
-
-end GroveStdlib.Std.CoreTypesAndOperations

doc/std/grove/GroveStdlib/Std/CoreTypesAndOperations/Containers.lean

@@ -1,110 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel
--/
-import Grove.Framework
-
-open Grove.Framework Widget
-
-namespace GroveStdlib.Std.CoreTypesAndOperations
-
-namespace Containers
-
-namespace SequentialContainers
-
-end SequentialContainers
-
-def sequentialContainers : Node :=
-  .section "sequential-containers" "Sequential containers" #[]
-
-namespace AssociativeContainers
-
-def associativeContainers : List Lean.Name :=
-  [`Std.DHashMap, `Std.DHashMap.Raw, `Std.ExtDHashMap, `Std.DTreeMap, `Std.DTreeMap.Raw, `Std.ExtDTreeMap, `Std.HashMap,
-   `Std.HashMap.Raw, `Std.ExtHashMap, `Std.TreeMap, `Std.TreeMap.Raw, `Std.ExtTreeMap, `Std.HashSet, `Std.HashSet.Raw, `Std.ExtHashSet,
-   `Std.TreeSet, `Std.TreeSet.Raw, `Std.ExtTreeSet]
-
-def associativeQueryOperations : AssociationTable .subexpression associativeContainers where
-  id := "associative-query-operations"
-  title := "Associative query operations"
-  description := "Operations that take as input an associative container and return a 'single' piece of information (e.g., `GetElem` or `isEmpty`, but not `toList`)."
-  dataSources n :=
-    (DataSource.definitionsInNamespace n)
-      |>.map Subexpression.declaration
-      |>.or (DataSource.getElem n)
-
-def associativeCreationOperations : AssociationTable .subexpression associativeContainers where
-  id := "associative-creation-operations"
-  title := "Associative creation operations"
-  description := "Operations that create a new associative container"
-  dataSources n :=
-    (DataSource.definitionsInNamespace n)
-      |>.map Subexpression.declaration
-      |>.or (DataSource.emptyCollection n)
-
-def associativeModificationOperations : AssociationTable .subexpression associativeContainers where
-  id := "associative-modification-operations"
-  title := "Associative modification operations"
-  description := "Operations that both accept and return an associative container"
-  dataSources n :=
-    (DataSource.definitionsInNamespace n)
-      |>.map Subexpression.declaration
-
-def associativeCreateThenQuery : Table .subexpression .subexpression .declaration associativeContainers where
-  id := "associative-create-then-query"
-  title := "Associative create then query"
-  description := "Lemmas that say what happens when creating a new associative container and then immediately querying from it"
-  rowsFrom := .table associativeCreationOperations
-  columnsFrom := .table associativeQueryOperations
-  cellData := .classic _ { relevantNamespaces := associativeContainers }
-
-def allOperationsCovered : Assertion where
-  widgetId := "associative-all-operations-covered"
-  title := "All operations on associative containers covered"
-  description := "All operations on an associative container should appear in at least one of the tables"
-  check := do
-    let allValuesArray : Array String ← #[associativeQueryOperations, associativeCreationOperations, associativeModificationOperations].flatMapM valuesInAssociationTable
-    let allValues : Std.HashSet String := Std.HashSet.ofArray allValuesArray
-    let env ← Lean.getEnv
-    let mut numBad := 0
-    for (n, _) in env.constants do
-      if associativeContainers.any (fun namesp => namesp.isPrefixOf n) then
-        if !n.toString ∈ allValues then
-          numBad := numBad + 1
-    return #[{
-      assertionId := "all-covered"
-      description := "All operations should be covered"
-      passed := numBad == 0
-      message := if numBad = 0 then "All operations were covered" else s!"There were {numBad} operations that were not covered."
-    }]
-
-end AssociativeContainers
-
-open AssociativeContainers in
-def associativeContainers : Node :=
-  .section "associative-containers" "Associative containers" #[
-    .associationTable associativeQueryOperations,
-    .associationTable associativeCreationOperations,
-    .associationTable associativeModificationOperations,
-    .table associativeCreateThenQuery,
-    .assertion allOperationsCovered
-  ]
-
-namespace PersistentDataStructures
-
-end PersistentDataStructures
-
-def persistentDataStructures : Node :=
-  .section "persistent-data-structures" "Persistent data structures" #[]
-
-end Containers
-
-def containers : Node :=
-  .section "containers" "Containers" #[
-    Containers.sequentialContainers,
-    Containers.associativeContainers,
-    Containers.persistentDataStructures
-  ]
-
-end GroveStdlib.Std.CoreTypesAndOperations

doc/std/grove/GroveStdlib/Std/CoreTypesAndOperations/Numbers.lean

@@ -1,19 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel
--/
-import Grove.Framework
-
-open Grove.Framework Widget
-
-namespace GroveStdlib.Std.CoreTypesAndOperations
-
-namespace Numbers
-
-end Numbers
-
-def numbers : Node :=
-  .section "numbers" "Numbers" #[]
-
-end GroveStdlib.Std.CoreTypesAndOperations

doc/std/grove/GroveStdlib/Std/CoreTypesAndOperations/StringsAndFormatting.lean

@@ -1,19 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel
--/
-import Grove.Framework
-
-open Grove.Framework Widget
-
-namespace GroveStdlib.Std.CoreTypesAndOperations
-
-namespace StringsAndFormatting
-
-end StringsAndFormatting
-
-def stringsAndFormatting : Node :=
-  .section "strings-and-formatting" "Strings and formatting" #[]
-
-end GroveStdlib.Std.CoreTypesAndOperations

doc/std/grove/GroveStdlib/Std/LanguageConstructs.lean

@@ -1,26 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel
--/
-import Grove.Framework
-import GroveStdlib.Std.LanguageConstructs.ComparisonOrderingHashing
-import GroveStdlib.Std.LanguageConstructs.Monads
-import GroveStdlib.Std.LanguageConstructs.RangesAndIterators
-
-open Grove.Framework Widget
-
-namespace GroveStdlib.Std
-
-namespace LanguageConstructs
-
-end LanguageConstructs
-
-def languageConstructs : Node :=
-  .section "language-constructs" "Language constructs" #[
-    LanguageConstructs.comparisonOrderingHashing,
-    LanguageConstructs.monads,
-    LanguageConstructs.rangesAndIterators
-  ]
-
-end GroveStdlib.Std

doc/std/grove/GroveStdlib/Std/LanguageConstructs/ComparisonOrderingHashing.lean

@@ -1,19 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel
--/
-import Grove.Framework
-
-open Grove.Framework Widget
-
-namespace GroveStdlib.Std.LanguageConstructs
-
-namespace ComparisonOrderingHashing
-
-end ComparisonOrderingHashing
-
-def comparisonOrderingHashing : Node :=
-  .section "comparison-ordering-hashing" "Comparison, ordering, hashing" #[]
-
-end GroveStdlib.Std.LanguageConstructs

doc/std/grove/GroveStdlib/Std/LanguageConstructs/Monads.lean

@@ -1,19 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel
--/
-import Grove.Framework
-
-open Grove.Framework Widget
-
-namespace GroveStdlib.Std.LanguageConstructs
-
-namespace Monads
-
-end Monads
-
-def monads : Node :=
-  .section "monads" "Monads" #[]
-
-end GroveStdlib.Std.LanguageConstructs

doc/std/grove/GroveStdlib/Std/LanguageConstructs/RangesAndIterators.lean

@@ -1,19 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel
--/
-import Grove.Framework
-
-open Grove.Framework Widget
-
-namespace GroveStdlib.Std.LanguageConstructs
-
-namespace RangesAndIterators
-
-end RangesAndIterators
-
-def rangesAndIterators : Node :=
-  .section "ranges-and-iterators" "Ranges and iterators" #[]
-
-end GroveStdlib.Std.LanguageConstructs

doc/std/grove/GroveStdlib/Std/Libraries.lean

@@ -1,24 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel
--/
-import Grove.Framework
-import GroveStdlib.Std.Libraries.DateAndTime
-import GroveStdlib.Std.Libraries.RandomNumbers
-
-open Grove.Framework Widget
-
-namespace GroveStdlib.Std
-
-namespace Libraries
-
-end Libraries
-
-def libraries : Node :=
-  .section "libraries" "Libraries" #[
-    Libraries.dateAndTime,
-    Libraries.randomNumbers
-  ]
-
-end GroveStdlib.Std

doc/std/grove/GroveStdlib/Std/Libraries/DateAndTime.lean

@@ -1,19 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel
--/
-import Grove.Framework
-
-open Grove.Framework Widget
-
-namespace GroveStdlib.Std.Libraries
-
-namespace DateAndTime
-
-end DateAndTime
-
-def dateAndTime : Node :=
-  .section "date-and-time" "Date and time" #[]
-
-end GroveStdlib.Std.Libraries

doc/std/grove/GroveStdlib/Std/Libraries/RandomNumbers.lean

@@ -1,19 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel
--/
-import Grove.Framework
-
-open Grove.Framework Widget
-
-namespace GroveStdlib.Std.Libraries
-
-namespace RandomNumbers
-
-end RandomNumbers
-
-def randomNumbers : Node :=
-  .section "random-numbers" "Random numbers" #[]
-
-end GroveStdlib.Std.Libraries

doc/std/grove/GroveStdlib/Std/OperatingSystemAbstractions.lean

@@ -1,30 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel
--/
-import Grove.Framework
-import GroveStdlib.Std.OperatingSystemAbstractions.AsynchronousIO
-import GroveStdlib.Std.OperatingSystemAbstractions.BasicIO
-import GroveStdlib.Std.OperatingSystemAbstractions.ConcurrencyAndParallelism
-import GroveStdlib.Std.OperatingSystemAbstractions.EnvironmentFileSystemProcesses
-import GroveStdlib.Std.OperatingSystemAbstractions.Locales
-
-open Grove.Framework Widget
-
-namespace GroveStdlib.Std
-
-namespace OperatingSystemAbstractions
-
-end OperatingSystemAbstractions
-
-def operatingSystemAbstractions : Node :=
-  .section "operating-system-abstractions" "Operating system abstractions" #[
-    OperatingSystemAbstractions.asynchronousIO,
-    OperatingSystemAbstractions.basicIO,
-    OperatingSystemAbstractions.concurrencyAndParallelism,
-    OperatingSystemAbstractions.environmentFileSystemProcesses,
-    OperatingSystemAbstractions.locales
-  ]
-
-end GroveStdlib.Std

doc/std/grove/GroveStdlib/Std/OperatingSystemAbstractions/AsynchronousIO.lean

@@ -1,19 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel
--/
-import Grove.Framework
-
-open Grove.Framework Widget
-
-namespace GroveStdlib.Std.OperatingSystemAbstractions
-
-namespace AsynchronousIO
-
-end AsynchronousIO
-
-def asynchronousIO : Node :=
-  .section "asynchronous-io" "Asynchronous I/O" #[]
-
-end GroveStdlib.Std.OperatingSystemAbstractions

doc/std/grove/GroveStdlib/Std/OperatingSystemAbstractions/BasicIO.lean

@@ -1,19 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel
--/
-import Grove.Framework
-
-open Grove.Framework Widget
-
-namespace GroveStdlib.Std.OperatingSystemAbstractions
-
-namespace BasicIO
-
-end BasicIO
-
-def basicIO : Node :=
-  .section "basic-io" "Basic I/O" #[]
-
-end GroveStdlib.Std.OperatingSystemAbstractions

doc/std/grove/GroveStdlib/Std/OperatingSystemAbstractions/ConcurrencyAndParallelism.lean

@@ -1,19 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel
--/
-import Grove.Framework
-
-open Grove.Framework Widget
-
-namespace GroveStdlib.Std.OperatingSystemAbstractions
-
-namespace ConcurrencyAndParallelism
-
-end ConcurrencyAndParallelism
-
-def concurrencyAndParallelism : Node :=
-  .section "concurrency-and-parallelism" "Concurrency and parallelism" #[]
-
-end GroveStdlib.Std.OperatingSystemAbstractions

doc/std/grove/GroveStdlib/Std/OperatingSystemAbstractions/EnvironmentFileSystemProcesses.lean

@@ -1,19 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel
--/
-import Grove.Framework
-
-open Grove.Framework Widget
-
-namespace GroveStdlib.Std.OperatingSystemAbstractions
-
-namespace EnvironmentFileSystemProcesses
-
-end EnvironmentFileSystemProcesses
-
-def environmentFileSystemProcesses : Node :=
-  .section "environment-filesystem-processes" "Environment, file system, processes" #[]
-
-end GroveStdlib.Std.OperatingSystemAbstractions

doc/std/grove/GroveStdlib/Std/OperatingSystemAbstractions/Locales.lean

@@ -1,19 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel
--/
-import Grove.Framework
-
-open Grove.Framework Widget
-
-namespace GroveStdlib.Std.OperatingSystemAbstractions
-
-namespace Locales
-
-end Locales
-
-def locales : Node :=
-  .section "locales" "Locales" #[]
-
-end GroveStdlib.Std.OperatingSystemAbstractions

doc/std/grove/Main.lean

@@ -1,18 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel
--/
-import GroveStdlib.Std
-import GroveStdlib.Generated
-
-def config : Grove.Framework.Project.Configuration where
-  projectNamespace := `GroveStdlib
-
-def project : Grove.Framework.Project where
-  config := config
-  rootNode := GroveStdlib.std
-  restoreState := GroveStdlib.Generated.restoreState
-
-def main (args : List String) : IO UInt32 :=
-  Grove.Framework.main project #[`Init, `Std, `Lean] args

doc/std/grove/README.md

@@ -1,3 +0,0 @@
-# Standard library QA
-
-This directory contains the [Grove](github.com/TwoFX/grove) data files for the standard library.

doc/std/grove/grove-local.sh

@@ -1,12 +0,0 @@
-#!/bin/sh
-
-lake exe grove-stdlib --full metadata.json
-cd .lake/packages/grove/frontend
-npm install
-cp ../../../../metadata.json public/metadata.json
-if [ -f "../../../../invalidated.json" ]; then
-    cp ../../../../invalidated.json public/invalidated.json
-    GROVE_DATA_LOCATION=public/metadata.json GROVE_UPSTREAM_INVALIDATED_FACTS_LOCATION=public/invalidated.json npm run dev
-else
-    GROVE_DATA_LOCATION=public/metadata.json npm run dev
-fi

doc/std/grove/lake-manifest.json

@@ -1,25 +0,0 @@
-{"version": "1.1.0",
- "packagesDir": ".lake/packages",
- "packages":
- [{"url": "https://github.com/TwoFx/grove.git",
-   "type": "git",
-   "subDir": "backend",
-   "scope": "",
-   "rev": "3e8aabdea58c11813c5d3b7eeb187ded44ee9a34",
-   "name": "grove",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
-   "inherited": false,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover/lean4-cli",
-   "type": "git",
-   "subDir": null,
-   "scope": "leanprover",
-   "rev": "1604206fcd0462da9a241beeac0e2df471647435",
-   "name": "Cli",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.toml"}],
- "name": "grovestdlib",
- "lakeDir": ".lake"}

doc/std/grove/lakefile.toml

@@ -1,18 +0,0 @@
-name = "grovestdlib"
-version = "0.1.0"
-defaultTargets = ["grove-stdlib"]
-
-[[require]]
-name = "grove"
-git = "https://github.com/TwoFx/grove.git"
-rev = "master"
-subDir = "backend"
-
-[[lean_lib]]
-name = "GroveStdlib"
-root = "GroveStdlib"
-
-[[lean_exe]]
-name = "grove-stdlib"
-supportInterpreter = true
-root = "Main"

doc/std/grove/lean-toolchain

@@ -1 +0,0 @@
-lean4

doc/std/grove/update_invalidated.sh

@@ -1,3 +0,0 @@
-#!/bin/sh
-
-lake exe grove-stdlib --invalidated invalidated.json

script/AnalyzeGrindAnnotations.lean

@@ -1,87 +0,0 @@
-/-
-Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-import Lean
-
-namespace Lean.Meta.Grind.Analyzer
-/-!
-A simple E-matching annotation analyzer.
-For each theorem annotated as an E-matching candidate, it creates an artificial goal, executes `grind` and shows the
-number of instances created.
-For a theorem of the form `params -> type`, the artificial goal is of the form `params -> type -> False`.
--/
-
-/--
-`grind` configuration for the analyzer. We disable case-splits and lookahead,
-increase the number of generations, and limit the number of instances generated.
--/
-def config : Grind.Config := {
-  splits       := 0
-  lookahead    := false
-  mbtc         := false
-  ematch       := 20
-  instances    := 100
-  gen          := 10
-}
-
-structure Config where
-  /-- Minimum number of instantiations to trigger summary report -/
-  min : Nat := 10
-  /-- Minimum number of instantiations to trigger detailed report -/
-  detailed : Nat := 50
-
-def mkParams : MetaM Params := do
-  let params ← Grind.mkParams config
-  let ematch ← getEMatchTheorems
-  let casesTypes ← Grind.getCasesTypes
-  return { params with ematch, casesTypes }
-
-/-- Returns the total number of generated instances.  -/
-private def sum (cs : PHashMap Origin Nat) : Nat := Id.run do
-  let mut r := 0
-  for (_, c) in cs do
-    r := r + c
-  return r
-
-private def thmsToMessageData (thms : PHashMap Origin Nat) : MetaM MessageData := do
-  let data := thms.toArray.filterMap fun (origin, c) =>
-    match origin with
-    | .decl declName => some (declName, c)
-    | _ => none
-  let data := data.qsort fun (d₁, c₁) (d₂, c₂) => if c₁ == c₂ then Name.lt d₁ d₂ else c₁ > c₂
-  let data ← data.mapM fun (declName, counter) =>
-    return .trace { cls := `thm } m!"{.ofConst (← mkConstWithLevelParams declName)} ↦ {counter}" #[]
-  return .trace { cls := `thm } "instances" data
-
-/--
-Analyzes theorem `declName`. That is, creates the artificial goal based on `declName` type,
-and invokes `grind` on it.
--/
-def analyzeEMatchTheorem (declName : Name) (c : Config) : MetaM Unit := do
-  let info ← getConstInfo declName
-  let mvarId ← forallTelescope info.type fun _ type => do
-    withLocalDeclD `h type fun _ => do
-      return (← mkFreshExprMVar (mkConst ``False)).mvarId!
-  let result ← Grind.main mvarId (← mkParams) (pure ())
-  let thms := result.counters.thm
-  let s := sum thms
-  if s > c.min then
-    IO.println s!"{declName} : {s}"
-  if s > c.detailed then
-    logInfo m!"{declName}\n{← thmsToMessageData thms}"
-
-/-- Analyzes all theorems in the standard library marked as E-matching theorems. -/
-def analyzeEMatchTheorems (c : Config := {}) : MetaM Unit := do
-  let origins := (← getEMatchTheorems).getOrigins
-  for o in origins do
-    let .decl declName := o | pure ()
-    analyzeEMatchTheorem declName c
-
-set_option maxHeartbeats 5000000
-run_meta analyzeEMatchTheorems
-
--- We can analyze specific theorems using commands such as
-set_option trace.grind.ematch.instance true in
-run_meta analyzeEMatchTheorem ``List.filterMap_some {}

script/bench.sh

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

script/mathlib-bench

@@ -5,11 +5,8 @@ set -euo pipefail
 
 [ $# -eq 1 ] || (echo "usage: $0 <lean4 PR #>"; exit 1)
 
-echo "Warning: the speedcenter is probably not listening on mathlib4-nightly-testing yet."
-echo "If you're using this script, please contact @kim-em or @Kha to get this set up, and then remove this notice."
-
 LEAN_PR=$1
-PR_RESPONSE=$(gh api repos/leanprover-community/mathlib4-nightly-testing/pulls -X POST -f head=lean-pr-testing-$LEAN_PR -f base=nightly-testing -f title="leanprover/lean4#$LEAN_PR benchmarking" -f draft=true -f body="ignore me")
+PR_RESPONSE=$(gh api repos/leanprover-community/mathlib4/pulls -X POST -f head=lean-pr-testing-$LEAN_PR -f base=nightly-testing -f title="leanprover/lean4#$LEAN_PR benchmarking" -f draft=true -f body="ignore me")
 PR_NUMBER=$(echo "$PR_RESPONSE" | jq '.number')
-echo "opened https://github.com/leanprover-community/mathlib4-nightly-testing/pull/$PR_NUMBER"
-gh api repos/leanprover-community/mathlib4-nightly-testing/issues/$PR_NUMBER/comments -X POST -f body="!bench" > /dev/null
+echo "opened https://github.com/leanprover-community/mathlib4/pull/$PR_NUMBER"
+gh api repos/leanprover-community/mathlib4/issues/$PR_NUMBER/comments -X POST -f body="!bench" > /dev/null

script/push_repo_release_tag.py

@@ -3,32 +3,6 @@ import sys
 import subprocess
 import requests
 
-def check_gh_auth():
-    """Check if GitHub CLI is properly authenticated."""
-    try:
-        result = subprocess.run(["gh", "auth", "status"], capture_output=True, text=True)
-        if result.returncode != 0:
-            return False, result.stderr
-        return True, None
-    except FileNotFoundError:
-        return False, "GitHub CLI (gh) is not installed. Please install it first."
-    except Exception as e:
-        return False, f"Error checking authentication: {e}"
-
-def handle_gh_error(error_output):
-    """Handle GitHub CLI errors and provide helpful messages."""
-    if "Not Found (HTTP 404)" in error_output:
-        return "Repository not found or access denied. Please check:\n" \
-               "1. The repository name is correct\n" \
-               "2. You have access to the repository\n" \
-               "3. Your GitHub CLI authentication is valid"
-    elif "Bad credentials" in error_output or "invalid" in error_output.lower():
-        return "Authentication failed. Please run 'gh auth login' to re-authenticate."
-    elif "rate limit" in error_output.lower():
-        return "GitHub API rate limit exceeded. Please try again later."
-    else:
-        return f"GitHub API error: {error_output}"
-
 def main():
     if len(sys.argv) != 4:
         print("Usage: ./push_repo_release_tag.py <repo> <branch> <version_tag>")
@@ -40,13 +14,6 @@ def main():
         print(f"Error: Branch '{branch}' is not 'master' or 'main'.")
         sys.exit(1)
 
-    # Check GitHub CLI authentication first
-    auth_ok, auth_error = check_gh_auth()
-    if not auth_ok:
-        print(f"Authentication error: {auth_error}")
-        print("\nTo fix this, run: gh auth login")
-        sys.exit(1)
-
     # Get the `lean-toolchain` file content
     lean_toolchain_url = f"https://raw.githubusercontent.com/{repo}/{branch}/lean-toolchain"
     try:
@@ -76,23 +43,12 @@ def main():
                 for tag in existing_tags:
                     print(tag.replace("refs/tags/", ""))
                 sys.exit(1)
-        elif list_tags_output.returncode != 0:
-            # Handle API errors when listing tags
-            error_msg = handle_gh_error(list_tags_output.stderr)
-            print(f"Error checking existing tags: {error_msg}")
-            sys.exit(1)
 
         # Get the SHA of the branch
         get_sha_cmd = [
             "gh", "api", f"repos/{repo}/git/ref/heads/{branch}", "--jq", ".object.sha"
         ]
-        sha_result = subprocess.run(get_sha_cmd, capture_output=True, text=True)
-        
-        if sha_result.returncode != 0:
-            error_msg = handle_gh_error(sha_result.stderr)
-            print(f"Error getting branch SHA: {error_msg}")
-            sys.exit(1)
-            
+        sha_result = subprocess.run(get_sha_cmd, capture_output=True, text=True, check=True)
         sha = sha_result.stdout.strip()
 
         # Create the tag
@@ -102,20 +58,11 @@ def main():
             "-F", f"ref=refs/tags/{version_tag}",
             "-F", f"sha={sha}"
         ]
-        create_result = subprocess.run(create_tag_cmd, capture_output=True, text=True)
-        
-        if create_result.returncode != 0:
-            error_msg = handle_gh_error(create_result.stderr)
-            print(f"Error creating tag: {error_msg}")
-            sys.exit(1)
+        subprocess.run(create_tag_cmd, capture_output=True, text=True, check=True)
 
         print(f"Successfully created and pushed tag '{version_tag}' to {repo}.")
     except subprocess.CalledProcessError as e:
-        error_msg = handle_gh_error(e.stderr.strip() if e.stderr else str(e))
-        print(f"Error while creating/pushing tag: {error_msg}")
-        sys.exit(1)
-    except Exception as e:
-        print(f"Unexpected error: {e}")
+        print(f"Error while creating/pushing tag: {e.stderr.strip() if e.stderr else e}")
         sys.exit(1)
 
 if __name__ == "__main__":

script/release_checklist.py

@@ -231,43 +231,6 @@ def get_next_version(version):
     # Next version is always .0
     return f"v{major}.{minor + 1}.0"
 
-def get_latest_nightly_tag(github_token):
-    """Get the most recent nightly tag from leanprover/lean4-nightly."""
-    api_url = "https://api.github.com/repos/leanprover/lean4-nightly/tags"
-    headers = {'Authorization': f'token {github_token}'} if github_token else {}
-    response = requests.get(api_url, headers=headers)
-    if response.status_code != 200:
-        return None
-    tags = response.json()
-    if not tags:
-        return None
-    # Return the most recent tag name
-    return tags[0]['name']
-
-def update_lean_toolchain_in_branch(org_repo, branch, toolchain_content, github_token):
-    """Update the lean-toolchain file in a specific branch."""
-    api_url = f"https://api.github.com/repos/{org_repo}/contents/lean-toolchain"
-    headers = {'Authorization': f'token {github_token}'} if github_token else {}
-    
-    # First get the current file to get its SHA
-    response = requests.get(f"{api_url}?ref={branch}", headers=headers)
-    if response.status_code != 200:
-        return False
-    
-    current_file = response.json()
-    file_sha = current_file['sha']
-    
-    # Update the file
-    update_data = {
-        "message": f"chore: update lean-toolchain to {toolchain_content}",
-        "content": base64.b64encode(toolchain_content.encode('utf-8')).decode('utf-8'),
-        "sha": file_sha,
-        "branch": branch
-    }
-    
-    response = requests.put(api_url, json=update_data, headers=headers)
-    return response.status_code in [200, 201]
-
 def check_bump_branch_toolchain(url, bump_branch, github_token):
     """Check if the lean-toolchain file in bump branch starts with either 'leanprover/lean4:nightly-' or the next version."""
     content = get_branch_content(url, bump_branch, "lean-toolchain", github_token)
@@ -299,61 +262,6 @@ def pr_exists_with_title(repo_url, title, github_token):
             return pr['number'], pr['html_url']
     return None
 
-def check_proofwidgets4_release(repo_url, target_toolchain, github_token):
-    """Check if ProofWidgets4 has a release tag that uses the target toolchain."""
-    api_base = repo_url.replace("https://github.com/", "https://api.github.com/repos/")
-    headers = {'Authorization': f'token {github_token}'} if github_token else {}
-    
-    # Get all tags matching v0.0.* pattern
-    response = requests.get(f"{api_base}/git/matching-refs/tags/v0.0.", headers=headers)
-    if response.status_code != 200:
-        print(f"  ❌ Could not fetch ProofWidgets4 tags")
-        return False
-    
-    tags = response.json()
-    if not tags:
-        print(f"  ❌ No v0.0.* tags found for ProofWidgets4")
-        return False
-    
-    # Extract tag names and sort by version number (descending)
-    tag_names = []
-    for tag in tags:
-        ref = tag['ref']
-        if ref.startswith('refs/tags/v0.0.'):
-            tag_name = ref.replace('refs/tags/', '')
-            try:
-                # Extract the number after v0.0.
-                version_num = int(tag_name.split('.')[-1])
-                tag_names.append((version_num, tag_name))
-            except (ValueError, IndexError):
-                continue
-    
-    if not tag_names:
-        print(f"  ❌ No valid v0.0.* tags found for ProofWidgets4")
-        return False
-    
-    # Sort by version number (descending) and take the most recent 10
-    tag_names.sort(reverse=True)
-    recent_tags = tag_names[:10]
-    
-    # Check each recent tag to see if it uses the target toolchain
-    for version_num, tag_name in recent_tags:
-        toolchain_content = get_branch_content(repo_url, tag_name, "lean-toolchain", github_token)
-        if toolchain_content is None:
-            continue
-        
-        if is_version_gte(toolchain_content.strip(), target_toolchain):
-            print(f"  ✅ Found release {tag_name} using compatible toolchain (>= {target_toolchain})")
-            return True
-    
-    # If we get here, no recent release uses the target toolchain
-    # Find the highest version number to suggest the next one
-    highest_version = max(version_num for version_num, _ in recent_tags)
-    next_version = highest_version + 1
-    print(f"  ❌ No recent ProofWidgets4 release uses toolchain >= {target_toolchain}")
-    print(f"     You will need to create and push a tag v0.0.{next_version}")
-    return False
-
 def main():
     parser = argparse.ArgumentParser(description="Check release status of Lean4 repositories")
     parser.add_argument("toolchain", help="The toolchain version to check (e.g., v4.6.0)")
@@ -478,12 +386,6 @@ def main():
             continue
         print(f"  ✅ On compatible toolchain (>= {toolchain})")
 
-        # Special handling for ProofWidgets4
-        if name == "ProofWidgets4":
-            if not check_proofwidgets4_release(url, toolchain, github_token):
-                repo_status[name] = False
-                continue
-
         if check_tag:
             tag_exists_initially = tag_exists(url, toolchain, github_token)
             if not tag_exists_initially:                
@@ -492,7 +394,7 @@ def main():
                     repo_status[name] = False
                     continue
                 else:
-                    print(f"  ⮕ Tag {toolchain} does not exist. Running `script/push_repo_release_tag.py {org_repo} {branch} {toolchain}`...")
+                    print(f"  … Tag {toolchain} does not exist. Running `script/push_repo_release_tag.py {org_repo} {branch} {toolchain}`...")
                     
                     # Run the script to create the tag
                     subprocess.run(["script/push_repo_release_tag.py", org_repo, branch, toolchain])
@@ -515,7 +417,7 @@ def main():
                     repo_status[name] = False
                     continue
                 else:
-                    print(f"  ⮕ Tag {toolchain} is not merged into stable. Running `script/merge_remote.py {org_repo} stable {toolchain}`...")
+                    print(f"  … Tag {toolchain} is not merged into stable. Running `script/merge_remote.py {org_repo} stable {toolchain}`...")
                     
                     # Run the script to merge the tag
                     subprocess.run(["script/merge_remote.py", org_repo, "stable", toolchain])
@@ -532,49 +434,19 @@ def main():
         if check_bump:
             next_version = get_next_version(toolchain)
             bump_branch = f"bump/{next_version}"
-            
-            # For mathlib4, use the nightly-testing fork for bump branches
-            bump_org_repo = org_repo
-            bump_url = url
-            if name == "mathlib4":
-                bump_org_repo = "leanprover-community/mathlib4-nightly-testing"
-                bump_url = "https://github.com/leanprover-community/mathlib4-nightly-testing"
-            
-            branch_created = False
-            if not branch_exists(bump_url, bump_branch, github_token):
+            if not branch_exists(url, bump_branch, github_token):
                 if args.dry_run:
-                    latest_nightly = get_latest_nightly_tag(github_token)
-                    nightly_note = f" (will set lean-toolchain to {latest_nightly})" if name in ["batteries", "mathlib4"] and latest_nightly else ""
-                    print(f"  ❌ Bump branch {bump_branch} does not exist. Run `gh api -X POST /repos/{bump_org_repo}/git/refs -f ref=refs/heads/{bump_branch} -f sha=$(gh api /repos/{org_repo}/git/refs/heads/{branch} --jq .object.sha)` to create it{nightly_note}.")
+                    print(f"  ❌ Bump branch {bump_branch} does not exist. Run `gh api -X POST /repos/{org_repo}/git/refs -f ref=refs/heads/{bump_branch} -f sha=$(gh api /repos/{org_repo}/git/refs/heads/{branch} --jq .object.sha)` to create it.")
                     repo_status[name] = False
                     continue
-                print(f"  ⮕ Bump branch {bump_branch} does not exist. Creating it...")
-                result = run_command(f"gh api -X POST /repos/{bump_org_repo}/git/refs -f ref=refs/heads/{bump_branch} -f sha=$(gh api /repos/{org_repo}/git/refs/heads/{branch} --jq .object.sha)", check=False)
+                print(f"  … Bump branch {bump_branch} does not exist. Creating it...")
+                result = run_command(f"gh api -X POST /repos/{org_repo}/git/refs -f ref=refs/heads/{bump_branch} -f sha=$(gh api /repos/{org_repo}/git/refs/heads/{branch} --jq .object.sha)", check=False)
                 if result.returncode != 0:
                     print(f"  ❌ Failed to create bump branch {bump_branch}")
                     repo_status[name] = False
                     continue
-                branch_created = True
-            
             print(f"  ✅ Bump branch {bump_branch} exists")
-            
-            # For batteries and mathlib4, update the lean-toolchain to the latest nightly
-            if branch_created and name in ["batteries", "mathlib4"]:
-                latest_nightly = get_latest_nightly_tag(github_token)
-                if latest_nightly:
-                    nightly_toolchain = f"leanprover/lean4:{latest_nightly}"
-                    print(f"  ⮕ Updating lean-toolchain to {nightly_toolchain}...")
-                    if update_lean_toolchain_in_branch(bump_org_repo, bump_branch, nightly_toolchain, github_token):
-                        print(f"  ✅ Updated lean-toolchain to {nightly_toolchain}")
-                    else:
-                        print(f"  ❌ Failed to update lean-toolchain to {nightly_toolchain}")
-                        repo_status[name] = False
-                        continue
-                else:
-                    print(f"  ❌ Could not fetch latest nightly tag")
-                    repo_status[name] = False
-                    continue
-            if not check_bump_branch_toolchain(bump_url, bump_branch, github_token):
+            if not check_bump_branch_toolchain(url, bump_branch, github_token):
                 repo_status[name] = False
                 continue
 

script/release_repos.yml

@@ -28,28 +28,6 @@ repositories:
     branch: main
     dependencies: []
 
-  - name: verso
-    url: https://github.com/leanprover/verso
-    toolchain-tag: true
-    stable-branch: false
-    branch: main
-    dependencies: []
-
-  - name: plausible
-    url: https://github.com/leanprover-community/plausible
-    toolchain-tag: true
-    stable-branch: false
-    branch: main
-    dependencies: []
-
-  - name: import-graph
-    url: https://github.com/leanprover-community/import-graph
-    toolchain-tag: true
-    stable-branch: false
-    branch: main
-    dependencies:
-      - lean4-cli
-
   - name: doc-gen4
     url: https://github.com/leanprover/doc-gen4
     toolchain-tag: true
@@ -57,6 +35,13 @@ repositories:
     branch: main
     dependencies: [lean4-cli]
 
+  - name: verso
+    url: https://github.com/leanprover/verso
+    toolchain-tag: true
+    stable-branch: false
+    branch: main
+    dependencies: []
+
   - name: reference-manual
     url: https://github.com/leanprover/reference-manual
     toolchain-tag: true
@@ -80,6 +65,22 @@ repositories:
     dependencies:
       - batteries
 
+  - name: import-graph
+    url: https://github.com/leanprover-community/import-graph
+    toolchain-tag: true
+    stable-branch: false
+    branch: main
+    dependencies:
+      - lean4-cli
+      - batteries
+
+  - name: plausible
+    url: https://github.com/leanprover-community/plausible
+    toolchain-tag: true
+    stable-branch: false
+    branch: main
+    dependencies: []
+
   - name: mathlib4
     url: https://github.com/leanprover-community/mathlib4
     toolchain-tag: true

script/release_steps.py

@@ -1,10 +1,10 @@
 #!/usr/bin/env python3
 
 """
-Execute release steps for Lean4 repositories.
+Generate release steps script for Lean4 repositories.
 
 This script helps automate the release process for Lean4 and its dependent repositories
-by actually executing the step-by-step instructions for updating toolchains, creating tags,
+by generating step-by-step instructions for updating toolchains, creating tags,
 and managing branches.
 
 Usage:
@@ -12,11 +12,11 @@ Usage:
 
 Arguments:
     version: The version to set in the lean-toolchain file (e.g., v4.6.0)
-    repo: The repository name as specified in release_repos.yml
+    repo: A substring of the repository name as specified in release_repos.yml
 
 Example:
-    python3 release_steps.py v4.6.0 mathlib4
-    python3 release_steps.py v4.6.0 batteries
+    python3 release_steps.py v4.6.0 mathlib
+    python3 release_steps.py v4.6.0 batt
 
 The script reads repository configurations from release_repos.yml in the same directory.
 Each repository may have specific requirements for:
@@ -32,124 +32,23 @@ import yaml
 import os
 import sys
 import re
-import subprocess
-import shutil
-import json
-from pathlib import Path
-
-# Color functions for terminal output
-def blue(text):
-    """Blue text for 'I'm doing something' messages."""
-    return f"\033[94m{text}\033[0m"
-
-def green(text):
-    """Green text for 'successful step' messages."""
-    return f"\033[92m{text}\033[0m"
-
-def red(text):
-    """Red text for 'this looks bad' messages."""
-    return f"\033[91m{text}\033[0m"
-
-def yellow(text):
-    """Yellow text for warnings."""
-    return f"\033[93m{text}\033[0m"
-
-def run_command(cmd, cwd=None, check=True, stream_output=False):
-    """Run a shell command and return the result."""
-    print(blue(f"Running: {cmd}"))
-    try:
-        if stream_output:
-            # Stream output in real-time for long-running commands
-            result = subprocess.run(cmd, shell=True, cwd=cwd, check=check, text=True)
-            return result
-        else:
-            # Capture output for commands where we need to process the result
-            result = subprocess.run(cmd, shell=True, cwd=cwd, check=check, 
-                                  capture_output=True, text=True)
-            if result.stdout:
-                # Command output in plain white (default terminal color)
-                print(result.stdout)
-            return result
-    except subprocess.CalledProcessError as e:
-        print(red(f"Error running command: {cmd}"))
-        print(red(f"Exit code: {e.returncode}"))
-        if not stream_output:
-            print(f"Stdout: {e.stdout}")
-            print(f"Stderr: {e.stderr}")
-        raise
 
 def load_repos_config(file_path):
     with open(file_path, "r") as f:
         return yaml.safe_load(f)["repositories"]
 
-def find_repo(repo_name, config):
-    matching_repos = [r for r in config if r["name"] == repo_name]
+def find_repo(repo_substring, config):
+    pattern = re.compile(re.escape(repo_substring), re.IGNORECASE)
+    matching_repos = [r for r in config if pattern.search(r["name"])]
     if not matching_repos:
-        print(red(f"Error: No repository named '{repo_name}' found in configuration."))
-        available_repos = [r["name"] for r in config]
-        print(yellow(f"Available repositories: {', '.join(available_repos)}"))
+        print(f"Error: No repository matching '{repo_substring}' found in configuration.")
+        sys.exit(1)
+    if len(matching_repos) > 1:
+        print(f"Error: Multiple repositories matching '{repo_substring}' found in configuration: {', '.join(r['name'] for r in matching_repos)}")
         sys.exit(1)
     return matching_repos[0]
 
-def setup_downstream_releases_dir():
-    """Create the downstream_releases directory if it doesn't exist."""
-    downstream_dir = Path("downstream_releases")
-    if not downstream_dir.exists():
-        print(blue(f"Creating {downstream_dir} directory..."))
-        downstream_dir.mkdir()
-        print(green(f"Created {downstream_dir} directory"))
-    return downstream_dir
-
-def clone_or_update_repo(repo_url, repo_dir, downstream_dir):
-    """Clone the repository if it doesn't exist, or update it if it does."""
-    repo_path = downstream_dir / repo_dir
-    
-    if repo_path.exists():
-        print(blue(f"Repository {repo_dir} already exists, updating..."))
-        run_command("git fetch", cwd=repo_path)
-        print(green(f"Updated repository {repo_dir}"))
-    else:
-        print(blue(f"Cloning {repo_url} to {repo_path}..."))
-        run_command(f"git clone {repo_url}", cwd=downstream_dir)
-        print(green(f"Cloned repository {repo_dir}"))
-    
-    return repo_path
-
-def get_remotes_for_repo(repo_name):
-    """Get the appropriate remotes for bump and nightly-testing branches based on repository."""
-    if repo_name == "mathlib4":
-        return "nightly-testing", "nightly-testing"
-    else:
-        return "origin", "origin"
-
-def check_and_abort_merge(repo_path):
-    """Check if repository is in the middle of a merge and abort it if so."""
-    merge_head_file = repo_path / ".git" / "MERGE_HEAD"
-    
-    if merge_head_file.exists():
-        print(yellow(f"Repository {repo_path.name} is in the middle of a merge. Aborting merge..."))
-        run_command("git merge --abort", cwd=repo_path)
-        print(green("Merge aborted successfully"))
-        return True
-    
-    # Also check git status for other merge-related states
-    try:
-        result = run_command("git status --porcelain=v1", cwd=repo_path, check=False)
-        if result.returncode == 0:
-            # Check for unmerged paths (indicated by 'UU', 'AA', etc. in git status)
-            for line in result.stdout.splitlines():
-                if len(line) >= 2 and line[:2] in ['UU', 'AA', 'DD', 'AU', 'UA', 'DU', 'UD']:
-                    print(yellow(f"Repository {repo_path.name} has unmerged paths. Aborting merge..."))
-                    run_command("git merge --abort", cwd=repo_path)
-                    print(green("Merge aborted successfully"))
-                    return True
-    except subprocess.CalledProcessError:
-        # If git status fails, we'll let the main process handle it
-        pass
-    
-    return False
-
-def execute_release_steps(repo, version, config):
+def generate_script(repo, version, config):
     repo_config = find_repo(repo, config)
     repo_name = repo_config['name']
     repo_url = repo_config['url']
@@ -160,481 +59,92 @@ def execute_release_steps(repo, version, config):
     requires_tagging = repo_config.get("toolchain-tag", True)
     has_stable_branch = repo_config.get("stable-branch", True)
 
-    # Setup downstream releases directory
-    downstream_dir = setup_downstream_releases_dir()
-    
-    # Clone or update the repository
-    repo_path = clone_or_update_repo(repo_url, repo_dir, downstream_dir)
-    
-    # Special remote setup for mathlib4
-    if repo_name == "mathlib4":
-        print(blue("Setting up special remotes for mathlib4..."))
-        try:
-            # Check if nightly-testing remote already exists
-            result = run_command("git remote get-url nightly-testing", cwd=repo_path, check=False)
-            if result.returncode != 0:
-                # Add the nightly-testing remote
-                run_command("git remote add nightly-testing https://github.com/leanprover-community/mathlib4-nightly-testing.git", cwd=repo_path)
-                print(green("Added nightly-testing remote"))
-            else:
-                print(green("nightly-testing remote already exists"))
-            
-            # Fetch from the nightly-testing remote
-            run_command("git fetch nightly-testing", cwd=repo_path)
-            print(green("Fetched from nightly-testing remote"))
-        except subprocess.CalledProcessError as e:
-            print(red(f"Error setting up mathlib4 remotes: {e}"))
-            print(yellow("Continuing with default remote setup..."))
-    
-    print(blue(f"\n=== Executing release steps for {repo_name} ==="))
-    
-    # Check if repository is in the middle of a merge and abort it if necessary
-    check_and_abort_merge(repo_path)
-    
-    # Execute the release steps
-    run_command(f"git checkout {default_branch} && git pull", cwd=repo_path)
-    
-    # Special rc1 safety check for batteries and mathlib4 (before creating any branches)
-    if repo_name in ["batteries", "mathlib4"] and version.endswith('-rc1'):
-        print(blue("This repo has nightly-testing infrastructure"))
-        print(blue(f"Checking if nightly-testing can be safely merged into bump/{version.split('-rc')[0]}..."))
-        
-        # Get the base version (e.g., v4.6.0 from v4.6.0-rc1)
-        base_version = version.split('-rc')[0]
-        bump_branch = f"bump/{base_version}"
-        
-        # Determine which remote to use for bump and nightly-testing branches
-        bump_remote, nightly_remote = get_remotes_for_repo(repo_name)
-        
-        try:
-            # Fetch latest changes from the appropriate remote
-            run_command(f"git fetch {bump_remote}", cwd=repo_path)
-            
-            # Check if the bump branch exists
-            result = run_command(f"git show-ref --verify --quiet refs/remotes/{bump_remote}/{bump_branch}", cwd=repo_path, check=False)
-            if result.returncode != 0:
-                print(red(f"Bump branch {bump_remote}/{bump_branch} does not exist. Cannot perform safety check."))
-                print(yellow("Please ensure the bump branch exists before proceeding."))
-                return
-            
-            # Create a temporary branch for testing the merge
-            temp_branch = f"temp-merge-test-{base_version}"
-            
-            # Clean up any existing temp branch from previous runs
-            result = run_command(f"git show-ref --verify --quiet refs/heads/{temp_branch}", cwd=repo_path, check=False)
-            if result.returncode == 0:
-                print(blue(f"Cleaning up existing temp branch {temp_branch}..."))
-                # Make sure we're not on the temp branch before deleting it
-                run_command(f"git checkout {default_branch}", cwd=repo_path)
-                run_command(f"git branch -D {temp_branch}", cwd=repo_path)
-                print(green(f"Deleted existing temp branch {temp_branch}"))
-            
-            run_command(f"git checkout -b {temp_branch} {bump_remote}/{bump_branch}", cwd=repo_path)
-            
-            # Try to merge nightly-testing
-            try:
-                run_command(f"git merge {nightly_remote}/nightly-testing", cwd=repo_path)
-                
-                # Check what files have changed compared to the bump branch
-                changed_files = run_command(f"git diff --name-only {bump_remote}/{bump_branch}..HEAD", cwd=repo_path)
-                
-                # Filter out allowed changes
-                allowed_patterns = ['lean-toolchain', 'lake-manifest.json']
-                problematic_files = []
-                
-                for file in changed_files.stdout.strip().split('\n'):
-                    if file.strip():  # Skip empty lines
-                        is_allowed = any(pattern in file for pattern in allowed_patterns)
-                        if not is_allowed:
-                            problematic_files.append(file)
-                
-                # Clean up temporary branch and return to default branch
-                run_command(f"git checkout {default_branch}", cwd=repo_path)
-                run_command(f"git branch -D {temp_branch}", cwd=repo_path)
-                
-                if problematic_files:
-                    print(red("❌ Safety check failed!"))
-                    print(red(f"Merging nightly-testing into {bump_branch} would result in changes to:"))
-                    for file in problematic_files:
-                        print(red(f"  - {file}"))
-                    print(yellow("\nYou need to make a PR merging the changes from nightly-testing into the bump branch first."))
-                    print(yellow(f"Create a PR from nightly-testing targeting {bump_branch} to resolve these changes."))
-                    return
-                else:
-                    print(green("✅ Safety check passed - only lean-toolchain and/or lake-manifest.json would change"))
-                    
-            except subprocess.CalledProcessError:
-                # Merge failed due to conflicts - check which files are conflicted
-                print(blue("Merge failed, checking which files are affected..."))
-                
-                # Get all changed files using git status
-                status_result = run_command("git status --porcelain", cwd=repo_path)
-                changed_files = []
-                
-                for line in status_result.stdout.splitlines():
-                    if line.strip():  # Skip empty lines
-                        # Extract filename (skip the first 3 characters which are status codes)
-                        changed_files.append(line[3:])
-                
-                # Filter out allowed files
-                allowed_patterns = ['lean-toolchain', 'lake-manifest.json']
-                problematic_files = []
-                
-                for file in changed_files:
-                    is_allowed = any(pattern in file for pattern in allowed_patterns)
-                    if not is_allowed:
-                        problematic_files.append(file)
-                
-                if problematic_files:
-                    # There are changes in non-allowed files - fail the safety check
-                    # First abort the merge to clean up the conflicted state
-                    run_command("git merge --abort", cwd=repo_path)
-                    run_command(f"git checkout {default_branch}", cwd=repo_path)
-                    run_command(f"git branch -D {temp_branch}", cwd=repo_path)
-                    print(red("❌ Safety check failed!"))
-                    print(red(f"Merging nightly-testing into {bump_branch} would result in changes to:"))
-                    for file in problematic_files:
-                        print(red(f"  - {file}"))
-                    print(yellow("\nYou need to make a PR merging the changes from nightly-testing into the bump branch first."))
-                    print(yellow(f"Create a PR from nightly-testing targeting {bump_branch} to resolve these changes."))
-                    return
-                else:
-                    # Only allowed files are changed - resolve them and continue
-                    print(green(f"✅ Only allowed files changed: {', '.join(changed_files)}"))
-                    print(blue("Resolving conflicts by taking nightly-testing version..."))
-                    
-                    # For each changed allowed file, take the nightly-testing version
-                    for file in changed_files:
-                        run_command(f"git checkout --theirs {file}", cwd=repo_path)
-                    
-                    # Complete the merge
-                    run_command("git add .", cwd=repo_path)
-                    run_command("git commit --no-edit", cwd=repo_path)
-                    
-                    print(green("✅ Safety check passed - changes only in allowed files"))
-                
-                # Clean up temporary branch and return to default branch
-                run_command(f"git checkout {default_branch}", cwd=repo_path)
-                run_command(f"git branch -D {temp_branch}", cwd=repo_path)
-                
-        except subprocess.CalledProcessError as e:
-            # Ensure we're back on the default branch even if setup failed
-            try:
-                run_command(f"git checkout {default_branch}", cwd=repo_path)
-            except subprocess.CalledProcessError:
-                print(red(f"Cannot return to {default_branch} branch. Repository is in an inconsistent state."))
-                print(red("Please manually check the repository state and fix any issues."))
-                return
-            print(red(f"Error during safety check: {e}"))
-            print(yellow("Skipping safety check and proceeding with normal merge..."))
-    
-    # Check if the branch already exists
-    branch_name = f"bump_to_{version}"
-    try:
-        # Check if branch exists locally
-        result = run_command(f"git show-ref --verify --quiet refs/heads/{branch_name}", cwd=repo_path, check=False)
-        if result.returncode == 0:
-            print(blue(f"Branch {branch_name} already exists, checking it out..."))
-            run_command(f"git checkout {branch_name}", cwd=repo_path)
-            print(green(f"Checked out existing branch {branch_name}"))
-        else:
-            print(blue(f"Creating new branch {branch_name}..."))
-            run_command(f"git checkout -b {branch_name}", cwd=repo_path)
-            print(green(f"Created new branch {branch_name}"))
-    except subprocess.CalledProcessError:
-        print(blue(f"Creating new branch {branch_name}..."))
-        run_command(f"git checkout -b {branch_name}", cwd=repo_path)
-        print(green(f"Created new branch {branch_name}"))
-    
-    # Update lean-toolchain
-    print(blue("Updating lean-toolchain file..."))
-    toolchain_file = repo_path / "lean-toolchain"
-    with open(toolchain_file, "w") as f:
-        f.write(f"leanprover/lean4:{version}\n")
-    print(green(f"Updated lean-toolchain to leanprover/lean4:{version}"))
+    script_lines = [
+        f"cd {repo_dir}",
+        "git fetch",
+        f"git checkout {default_branch} && git pull",
+        f"git checkout -b bump_to_{version}",
+        f"echo leanprover/lean4:{version} > lean-toolchain",
+    ]
 
     # Special cases for specific repositories
     if repo_name == "repl":
-        run_command("lake update", cwd=repo_path, stream_output=True)
-        mathlib_test_dir = repo_path / "test" / "Mathlib"
-        run_command(f'perl -pi -e \'s/rev = "v\\d+\\.\\d+\\.\\d+(-rc\\d+)?"/rev = "{version}"/g\' lakefile.toml', cwd=mathlib_test_dir)
-        
-        # Update lean-toolchain in test/Mathlib
-        print(blue("Updating test/Mathlib/lean-toolchain..."))
-        mathlib_toolchain = mathlib_test_dir / "lean-toolchain"
-        with open(mathlib_toolchain, "w") as f:
-            f.write(f"leanprover/lean4:{version}\n")
-        print(green(f"Updated test/Mathlib/lean-toolchain to leanprover/lean4:{version}"))
-        
-        run_command("lake update", cwd=mathlib_test_dir, stream_output=True)
-        try:
-            result = run_command("./test.sh", cwd=repo_path, stream_output=True, check=False)
-            if result.returncode == 0:
-                print(green("Tests completed successfully"))
-            else:
-                print(red("Tests failed, but continuing with PR creation..."))
-                print(red(f"Test exit code: {result.returncode}"))
-        except subprocess.CalledProcessError as e:
-            print(red("Tests failed, but continuing with PR creation..."))
-            print(red(f"Test error: {e}"))
+        script_lines.extend([
+            "lake update",
+            "cd test/Mathlib",
+            f"perl -pi -e 's/rev = \"v\\d+\\.\\d+\\.\\d+(-rc\\d+)?\"/rev = \"{version}\"/g' lakefile.toml",
+            f"echo leanprover/lean4:{version} > lean-toolchain",
+            "lake update",
+            "cd ../..",
+            "./test.sh"
+        ])
     elif dependencies:
-        run_command(f'perl -pi -e \'s/"v4\\.[0-9]+(\\.[0-9]+)?(-rc[0-9]+)?"/"' + version + '"/g\' lakefile.*', cwd=repo_path)
-        run_command("lake update", cwd=repo_path, stream_output=True)
+        script_lines.append('perl -pi -e \'s/"v4\\.[0-9]+(\\.[0-9]+)?(-rc[0-9]+)?"/"' + version + '"/g\' lakefile.*')
+        script_lines.append("lake update")
 
-    # Commit changes (only if there are changes)
-    print(blue("Checking for changes to commit..."))
-    try:
-        # Check if there are any changes to commit (staged or unstaged)
-        result = run_command("git status --porcelain", cwd=repo_path, check=False)
-        if result.stdout.strip():  # There are changes
-            print(blue("Committing changes..."))
-            run_command(f'git commit -am "chore: bump toolchain to {version}"', cwd=repo_path)
-            print(green(f"Committed changes: chore: bump toolchain to {version}"))
-        else:
-            print(green("No changes to commit - toolchain already up to date"))
-    except subprocess.CalledProcessError:
-        print(yellow("Failed to check for changes, attempting commit anyway..."))
-        try:
-            run_command(f'git commit -am "chore: bump toolchain to {version}"', cwd=repo_path)
-        except subprocess.CalledProcessError as e:
-            if "nothing to commit" in e.stderr:
-                print(green("No changes to commit - toolchain already up to date"))
-            else:
-                raise
+    script_lines.append("")
 
-    # Handle special merging cases
-    if version.endswith('-rc1') and repo_name in ["batteries", "mathlib4"]:
-        print(blue("This repo uses `bump/v4.X.0` branches for reviewed content from nightly-testing."))
-        
-        # Determine which remote to use for bump branches
-        bump_remote, nightly_remote = get_remotes_for_repo(repo_name)
-        
-        # Fetch latest changes to ensure we have the most up-to-date bump branch
-        print(blue(f"Fetching latest changes from {bump_remote}..."))
-        run_command(f"git fetch {bump_remote}", cwd=repo_path)
-        
-        try:
-            print(blue(f"Merging {bump_remote}/bump/{version.split('-rc')[0]}..."))
-            run_command(f"git merge {bump_remote}/bump/{version.split('-rc')[0]}", cwd=repo_path)
-            print(green("Merge completed successfully"))
-        except subprocess.CalledProcessError:
-            # Merge failed due to conflicts - check which files are conflicted
-            print(blue("Merge conflicts detected, checking which files are affected..."))
-            
-            # Get conflicted files using git status
-            status_result = run_command("git status --porcelain", cwd=repo_path)
-            conflicted_files = []
-            
-            for line in status_result.stdout.splitlines():
-                if len(line) >= 2 and line[:2] in ['UU', 'AA', 'DD', 'AU', 'UA', 'DU', 'UD']:
-                    # Extract filename (skip the first 3 characters which are status codes)
-                    conflicted_files.append(line[3:])
-            
-            # Filter out allowed files
-            allowed_patterns = ['lean-toolchain', 'lake-manifest.json']
-            problematic_files = []
-            
-            for file in conflicted_files:
-                is_allowed = any(pattern in file for pattern in allowed_patterns)
-                if not is_allowed:
-                    problematic_files.append(file)
-            
-            if problematic_files:
-                # There are conflicts in non-allowed files - fail
-                print(red("❌ Merge failed!"))
-                print(red(f"Merging {bump_remote}/bump/{version.split('-rc')[0]} resulted in conflicts in:"))
-                for file in problematic_files:
-                    print(red(f"  - {file}"))
-                print(red("Please resolve these conflicts manually."))
-                return
-            else:
-                # Only allowed files are conflicted - resolve them automatically
-                print(green(f"✅ Only allowed files conflicted: {', '.join(conflicted_files)}"))
-                print(blue("Resolving conflicts automatically..."))
-                
-                # Overwrite lean-toolchain with our target version
-                if 'lean-toolchain' in conflicted_files:
-                    print(blue(f"Overwriting lean-toolchain with target version {version}"))
-                    toolchain_file = repo_path / "lean-toolchain"
-                    with open(toolchain_file, "w") as f:
-                        f.write(f"leanprover/lean4:{version}\n")
-                
-                # For other allowed files, take our version (since we want our changes)
-                for file in conflicted_files:
-                    if file != 'lean-toolchain':
-                        run_command(f"git checkout --ours {file}", cwd=repo_path)
-                
-                # Run lake update to rebuild lake-manifest.json
-                print(blue("Running lake update to rebuild lake-manifest.json..."))
-                run_command("lake update", cwd=repo_path, stream_output=True)
-                
-                # Complete the merge
-                run_command("git add .", cwd=repo_path)
-                run_command("git commit --no-edit", cwd=repo_path)
-                
-                print(green("✅ Merge completed successfully with automatic conflict resolution"))
-    
-    elif version.endswith('-rc1'):
-        # For all other repos with rc versions, merge nightly-testing
-        if repo_name in ["verso", "reference-manual"]:
-            print(yellow("This repo does development on nightly-testing: remember to rebase merge the PR."))
-        
-        # Fetch latest changes to ensure we have the most up-to-date nightly-testing branch
-        print(blue("Fetching latest changes from origin..."))
-        run_command("git fetch origin", cwd=repo_path)
-        
-        try:
-            print(blue("Merging origin/nightly-testing..."))
-            run_command("git merge origin/nightly-testing", cwd=repo_path)
-            print(green("Merge completed successfully"))
-        except subprocess.CalledProcessError:
-            # Merge failed due to conflicts - check which files are conflicted
-            print(blue("Merge conflicts detected, checking which files are affected..."))
-            
-            # Get conflicted files using git status
-            status_result = run_command("git status --porcelain", cwd=repo_path)
-            conflicted_files = []
-            
-            for line in status_result.stdout.splitlines():
-                if len(line) >= 2 and line[:2] in ['UU', 'AA', 'DD', 'AU', 'UA', 'DU', 'UD']:
-                    # Extract filename (skip the first 3 characters which are status codes)
-                    conflicted_files.append(line[3:])
-            
-            # Filter out allowed files
-            allowed_patterns = ['lean-toolchain', 'lake-manifest.json']
-            problematic_files = []
-            
-            for file in conflicted_files:
-                is_allowed = any(pattern in file for pattern in allowed_patterns)
-                if not is_allowed:
-                    problematic_files.append(file)
-            
-            if problematic_files:
-                # There are conflicts in non-allowed files - fail
-                print(red("❌ Merge failed!"))
-                print(red(f"Merging nightly-testing resulted in conflicts in:"))
-                for file in problematic_files:
-                    print(red(f"  - {file}"))
-                print(red("Please resolve these conflicts manually."))
-                return
-            else:
-                # Only allowed files are conflicted - resolve them automatically
-                print(green(f"✅ Only allowed files conflicted: {', '.join(conflicted_files)}"))
-                print(blue("Resolving conflicts automatically..."))
-                
-                # For lean-toolchain and lake-manifest.json, keep our versions
-                for file in conflicted_files:
-                    print(blue(f"Keeping our version of {file}"))
-                    run_command(f"git checkout --ours {file}", cwd=repo_path)
-                
-                # Complete the merge
-                run_command("git add .", cwd=repo_path)
-                run_command("git commit --no-edit", cwd=repo_path)
-                
-                print(green("✅ Merge completed successfully with automatic conflict resolution"))
+    script_lines.extend([
+        f'git commit -am "chore: bump toolchain to {version}"',
+        ""
+    ])
 
-    # Build and test (skip for Mathlib)
-    if repo_name not in ["mathlib4"]:
-        print(blue("Building project..."))
-        
-        # Clean lake cache for a fresh build
-        print(blue("Cleaning lake cache..."))
-        run_command("rm -rf .lake", cwd=repo_path)
-        
-        try:
-            run_command("lake build", cwd=repo_path, stream_output=True)
-            print(green("Build completed successfully"))
-        except subprocess.CalledProcessError as e:
-            print(red("Build failed, but continuing with PR creation..."))
-            print(red(f"Build error: {e}"))
-        
-        # Check if lake check-test exists before running tests
-        print(blue("Running tests..."))
-        check_test_result = run_command("lake check-test", cwd=repo_path, check=False)
-        if check_test_result.returncode == 0:
-            try:
-                run_command("lake test", cwd=repo_path, stream_output=True)
-                print(green("Tests completed successfully"))
-            except subprocess.CalledProcessError as e:
-                print(red("Tests failed, but continuing with PR creation..."))
-                print(red(f"Test error: {e}"))
-        else:
-            print(yellow("lake check-test reports that there is no test suite"))
+    if re.search(r'rc\d+$', version) and repo_name in ["batteries", "mathlib4"]:
+        script_lines.extend([
+            "echo 'This repo has nightly-testing infrastructure'",
+            f"git merge origin/bump/{version.split('-rc')[0]}",
+            "echo 'Please resolve any conflicts.'",
+            "grep nightly-testing lakefile.* && echo 'Please ensure the lakefile does not include nightly-testing versions.'",
+            ""
+        ])
+    if re.search(r'rc\d+$', version) and repo_name in ["verso", "reference-manual"]:
+        script_lines.extend([
+            "echo 'This repo does development on nightly-testing: remember to rebase merge the PR.'",
+            f"git merge origin/nightly-testing",
+            "echo 'Please resolve any conflicts.'",
+            ""
+        ])
+    if repo_name != "Mathlib":
+        script_lines.extend([
+            "lake build && if lake check-test; then lake test; fi",
+            ""
+        ])
 
-    # Push the branch to remote before creating PR
-    print(blue("Checking remote branch status..."))
-    try:
-        # Check if branch exists on remote
-        result = run_command(f"git ls-remote --heads origin {branch_name}", cwd=repo_path, check=False)
-        if not result.stdout.strip():
-            print(blue(f"Pushing branch {branch_name} to remote..."))
-            run_command(f"git push -u origin {branch_name}", cwd=repo_path)
-            print(green(f"Successfully pushed branch {branch_name} to remote"))
-        else:
-            print(blue(f"Branch {branch_name} already exists on remote, pushing any new commits..."))
-            run_command(f"git push", cwd=repo_path)
-            print(green("Successfully pushed commits to remote"))
-    except subprocess.CalledProcessError:
-        print(red("Failed to push branch to remote. Please check your permissions and network connection."))
-        print(yellow(f"You may need to run: git push -u origin {branch_name}"))
-        return
+    script_lines.extend([
+        'gh pr create --title "chore: bump toolchain to ' + version + '" --body ""',
+        "echo 'Please review the PR and merge or rebase it.'",
+        ""
+    ])
 
-    # Create pull request (only if one doesn't already exist)
-    print(blue("Checking for existing pull request..."))
-    try:
-        # Check if PR already exists for this branch
-        result = run_command(f'gh pr list --head {branch_name} --json number', cwd=repo_path, check=False)
-        if result.returncode == 0 and result.stdout.strip() != "[]":
-            print(green(f"Pull request already exists for branch {branch_name}"))
-            # Get the PR URL
-            pr_result = run_command(f'gh pr view {branch_name} --json url', cwd=repo_path, check=False)
-            if pr_result.returncode == 0:
-                pr_data = json.loads(pr_result.stdout)
-                print(green(f"PR URL: {pr_data.get('url', 'N/A')}"))
-        else:
-            # Create new PR
-            print(blue("Creating new pull request..."))
-            run_command(f'gh pr create --title "chore: bump toolchain to {version}" --body ""', cwd=repo_path)
-            print(green("Pull request created successfully!"))
-    except subprocess.CalledProcessError:
-        print(red("Failed to check for existing PR or create new PR."))
-        print(yellow("This could be due to:"))
-        print(yellow("1. GitHub CLI not authenticated"))
-        print(yellow("2. No push permissions to the repository"))
-        print(yellow("3. Network issues"))
-        print(f"Branch: {branch_name}")
-        print(f"Title: chore: bump toolchain to {version}")
-        print(yellow("Please create the PR manually if needed."))
+    return "\n".join(script_lines)
 
 def main():
     parser = argparse.ArgumentParser(
-        description="Execute release steps for Lean4 repositories.",
+        description="Generate release steps script for Lean4 repositories.",
         formatter_class=argparse.RawDescriptionHelpFormatter,
         epilog="""
 Examples:
-  %(prog)s v4.6.0 mathlib4   Execute steps for updating Mathlib to v4.6.0
-  %(prog)s v4.6.0 batteries  Execute steps for updating Batteries to v4.6.0
+  %(prog)s v4.6.0 mathlib    Generate steps for updating Mathlib to v4.6.0
+  %(prog)s v4.6.0 batt       Generate steps for updating Batteries to v4.6.0
   
-The script will:
-1. Create a downstream_releases/ directory
-2. Clone or update the target repository
-3. Update the lean-toolchain file
-4. Create appropriate branches and commits
-5. Build and test the project
-6. Create pull requests
+The script will generate shell commands to:
+1. Update the lean-toolchain file
+2. Create appropriate branches and commits
+3. Create pull requests
 
 (Note that the steps of creating toolchain version tags, and merging these into `stable` branches,
 are handled by `script/release_checklist.py`.)
 """
     )
     parser.add_argument("version", help="The version to set in the lean-toolchain file (e.g., v4.6.0)")
-    parser.add_argument("repo", help="The repository name as specified in release_repos.yml")
+    parser.add_argument("repo", help="A substring of the repository name as specified in release_repos.yml")
     args = parser.parse_args()
 
     config_path = os.path.join(os.path.dirname(__file__), "release_repos.yml")
     config = load_repos_config(config_path)
 
-    execute_release_steps(args.repo, args.version, config)
+    script = generate_script(args.repo, args.version, config)
+    print(script)
 
 if __name__ == "__main__":
     main()

src/CMakeLists.txt

@@ -10,7 +10,7 @@ endif()
 include(ExternalProject)
 project(LEAN CXX C)
 set(LEAN_VERSION_MAJOR 4)
-set(LEAN_VERSION_MINOR 23)
+set(LEAN_VERSION_MINOR 22)
 set(LEAN_VERSION_PATCH 0)
 set(LEAN_VERSION_IS_RELEASE 0)  # This number is 1 in the release revision, and 0 otherwise.
 set(LEAN_SPECIAL_VERSION_DESC "" CACHE STRING "Additional version description like 'nightly-2018-03-11'")
@@ -533,21 +533,12 @@ else()
         OUTPUT_VARIABLE GIT_SHA1
         OUTPUT_STRIP_TRAILING_WHITESPACE)
     message(STATUS "stage0 sha1: ${GIT_SHA1}")
-    # Now that we've prepared the information for the next stage, we can forget that we will use
-    # Lake in the future as we won't use it in this stage
-    set(USE_LAKE OFF)
   else()
     set(GIT_SHA1 "")
   endif()
 endif()
 configure_file("${LEAN_SOURCE_DIR}/githash.h.in" "${LEAN_BINARY_DIR}/githash.h")
 
-if(USE_LAKE AND ${STAGE} EQUAL 0)
-  # Now that we've prepared the information for the next stage, we can forget that we will use
-  # Lake in the future as we won't use it in this stage
-  set(USE_LAKE OFF)
-endif()
-
 # Windows uses ";" as a path separator. We use `LEAN_PATH_SEPARATOR` on scripts such as lean.mk.in
 if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
   set(LEAN_PATH_SEPARATOR ";")
@@ -643,6 +634,8 @@ else()
   set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:library>)
   add_subdirectory(library/constructions)
   set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:constructions>)
+  add_subdirectory(library/compiler)
+  set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:compiler>)
 
   # leancpp without `initialize` (see `leaninitialize` above)
   add_library(leancpp_1 STATIC ${LEAN_OBJS})
@@ -684,17 +677,12 @@ if (LLVM AND ${STAGE} GREATER 0)
   set(EXTRA_LEANMAKE_OPTS "LLVM=1")
 endif()
 
-set(STDLIBS Init Std Lean Leanc)
-if(NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
-  list(APPEND STDLIBS Lake)
-endif()
-
 add_custom_target(make_stdlib ALL
   WORKING_DIRECTORY ${LEAN_SOURCE_DIR}
   # The actual rule is in a separate makefile because we want to prefix it with '+' to use the Make job server
   # for a parallelized nested build, but CMake doesn't let us do that.
   # We use `lean` from the previous stage, but `leanc`, headers, etc. from the current stage
-  COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make ${STDLIBS}
+  COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make Init Std Lean Leanc
   VERBATIM)
 
 # if we have LLVM enabled, then build `lean.h.bc` which has the LLVM bitcode
@@ -738,9 +726,14 @@ else()
 endif()
 
 if(NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
-  add_custom_target(lake_shared
+  add_custom_target(lake_lib
     WORKING_DIRECTORY ${LEAN_SOURCE_DIR}
     DEPENDS leanshared
+    COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make Lake
+    VERBATIM)
+  add_custom_target(lake_shared
+    WORKING_DIRECTORY ${LEAN_SOURCE_DIR}
+    DEPENDS lake_lib
     COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make libLake_shared
     VERBATIM)
   add_custom_target(lake ALL
@@ -821,12 +814,6 @@ if(LEAN_INSTALL_PREFIX)
   set(CMAKE_INSTALL_PREFIX "${LEAN_INSTALL_PREFIX}/lean-${LEAN_VERSION_STRING}${LEAN_INSTALL_SUFFIX}")
 endif()
 
-if (STAGE GREATER 1)
-  # The build of stage2+ may depend on local changes made to src/ that are not reflected by the
-  # commit hash in stage1/bin/lean, so we make sure to disable the global cache
-  string(APPEND LEAN_EXTRA_LAKEFILE_TOML "\n\nenableArtifactCache = false")
-endif()
-
 # Escape for `make`. Yes, twice.
 string(REPLACE "$" "\\\$$" CMAKE_EXE_LINKER_FLAGS_MAKE "${CMAKE_EXE_LINKER_FLAGS}")
 configure_file(${LEAN_SOURCE_DIR}/stdlib.make.in ${CMAKE_BINARY_DIR}/stdlib.make)
@@ -853,10 +840,6 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
   set(LAKE_LIB_PREFIX "lib")
 endif()
 
-if(USE_LAKE)
-  configure_file(${LEAN_SOURCE_DIR}/lakefile.toml.in ${CMAKE_BINARY_DIR}/lakefile.toml)
-  # copy for editing
-  if(STAGE EQUAL 1)
-    configure_file(${LEAN_SOURCE_DIR}/lakefile.toml.in ${LEAN_SOURCE_DIR}/lakefile.toml)
-  endif()
+if(USE_LAKE AND STAGE EQUAL 1)
+  configure_file(${LEAN_SOURCE_DIR}/lakefile.toml.in ${LEAN_SOURCE_DIR}/lakefile.toml)
 endif()

src/Init.lean

@@ -6,41 +6,41 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Init.Prelude
-public import Init.Notation
-public import Init.Tactics
-public import Init.TacticsExtra
-public import Init.ByCases
-public import Init.RCases
-public import Init.Core
-public import Init.Control
-public import Init.Data.Basic
-public import Init.WF
-public import Init.WFTactics
-public import Init.Data
-public import Init.System
-public import Init.Util
-public import Init.Dynamic
-public import Init.ShareCommon
-public import Init.MetaTypes
-public import Init.Meta
-public import Init.NotationExtra
-public import Init.SimpLemmas
-public import Init.PropLemmas
-public import Init.Hints
-public import Init.Conv
-public import Init.Guard
-public import Init.Simproc
-public import Init.SizeOfLemmas
-public import Init.BinderPredicates
-public import Init.Ext
-public import Init.Omega
-public import Init.MacroTrace
-public import Init.Grind
-public import Init.GrindInstances
-public import Init.While
-public import Init.Syntax
-public import Init.Internal
-public import Init.Try
-public import Init.BinderNameHint
-public import Init.Task
+import Init.Prelude
+import Init.Notation
+import Init.Tactics
+import Init.TacticsExtra
+import Init.ByCases
+import Init.RCases
+import Init.Core
+import Init.Control
+import Init.Data.Basic
+import Init.WF
+import Init.WFTactics
+import Init.Data
+import Init.System
+import Init.Util
+import Init.Dynamic
+import Init.ShareCommon
+import Init.MetaTypes
+import Init.Meta
+import Init.NotationExtra
+import Init.SimpLemmas
+import Init.PropLemmas
+import Init.Hints
+import Init.Conv
+import Init.Guard
+import Init.Simproc
+import Init.SizeOfLemmas
+import Init.BinderPredicates
+import Init.Ext
+import Init.Omega
+import Init.MacroTrace
+import Init.Grind
+import Init.GrindInstances
+import Init.While
+import Init.Syntax
+import Init.Internal
+import Init.Try
+import Init.BinderNameHint
+import Init.Task

src/Init/BinderNameHint.lean

@@ -7,10 +7,8 @@ Authors: Joachim Breitner
 module
 
 prelude
-public import Init.Prelude
-public import Init.Tactics
-
-public section
+import Init.Prelude
+import Init.Tactics
 
 set_option linter.unusedVariables false in
 /--
@@ -39,7 +37,7 @@ This gadget is supported by
 * `simp`, `dsimp` and `rw` in the right-hand-side of an equation
 * `simp` in the assumptions of congruence rules
 
-It is ineffective in other positions (hypotheses of rewrite rules) or when used by other tactics
+It is ineffective in other positions (hyptheses of rewrite rules) or when used by other tactics
 (e.g. `apply`).
 -/
 @[simp ↓, expose]

src/Init/BinderPredicates.lean

@@ -6,9 +6,7 @@ Authors: Gabriel Ebner
 module
 
 prelude
-public import Init.NotationExtra
-
-public section
+import Init.NotationExtra
 
 namespace Lean
 

src/Init/ByCases.lean

@@ -6,9 +6,7 @@ Authors: Leonardo de Moura, Mario Carneiro
 module
 
 prelude
-public import Init.Classical
-
-public section
+import Init.Classical
 
 /-! # by_cases tactic and if-then-else support -/
 

src/Init/Classical.lean

@@ -6,9 +6,7 @@ Authors: Leonardo de Moura, Mario Carneiro
 module
 
 prelude
-public import Init.PropLemmas
-
-public section
+import Init.PropLemmas
 
 universe u v
 

src/Init/Coe.lean

@@ -6,10 +6,8 @@ Authors: Leonardo de Moura, Mario Carneiro
 module
 
 prelude
-public import Init.Prelude
-public meta import Init.Prelude
-
-public section
+import Init.Prelude
+meta import Init.Prelude
 set_option linter.missingDocs true -- keep it documented
 
 /-!

src/Init/Control.lean

@@ -6,15 +6,13 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Init.Control.Basic
-public import Init.Control.State
-public import Init.Control.StateRef
-public import Init.Control.Id
-public import Init.Control.Except
-public import Init.Control.Reader
-public import Init.Control.Option
-public import Init.Control.Lawful
-public import Init.Control.StateCps
-public import Init.Control.ExceptCps
-
-public section
+import Init.Control.Basic
+import Init.Control.State
+import Init.Control.StateRef
+import Init.Control.Id
+import Init.Control.Except
+import Init.Control.Reader
+import Init.Control.Option
+import Init.Control.Lawful
+import Init.Control.StateCps
+import Init.Control.ExceptCps

src/Init/Control/Basic.lean

@@ -6,10 +6,8 @@ Author: Leonardo de Moura, Sebastian Ullrich
 module
 
 prelude
-public import Init.Core
-public import Init.BinderNameHint
-
-@[expose] public section
+import Init.Core
+import Init.BinderNameHint
 
 universe u v w
 

src/Init/Control/EState.lean

@@ -6,11 +6,9 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Init.Control.State
-public import Init.Control.Except
-public import Init.Data.ToString.Basic
-
-public section
+import Init.Control.State
+import Init.Control.Except
+import Init.Data.ToString.Basic
 universe u v
 
 namespace EStateM

src/Init/Control/Except.lean

@@ -8,11 +8,9 @@ The Except monad transformer.
 module
 
 prelude
-public import Init.Control.Basic
-public import Init.Control.Id
-public import Init.Coe
-
-@[expose] public section
+import Init.Control.Basic
+import Init.Control.Id
+import Init.Coe
 
 namespace Except
 variable {ε : Type u}

src/Init/Control/ExceptCps.lean

@@ -6,9 +6,7 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Init.Control.Lawful.Basic
-
-public section
+import Init.Control.Lawful.Basic
 
 /-!
 The Exception monad transformer using CPS style.

src/Init/Control/Id.lean

@@ -8,9 +8,7 @@ The identity Monad.
 module
 
 prelude
-public import Init.Core
-
-public section
+import Init.Core
 
 universe u
 
@@ -64,7 +62,4 @@ protected def run (x : Id α) : α := x
 instance [OfNat α n] : OfNat (Id α) n :=
   inferInstanceAs (OfNat α n)
 
-instance {m : Type u → Type v} [Pure m] : MonadLiftT Id m where
-  monadLift x := pure x.run
-
 end Id

src/Init/Control/Lawful.lean

@@ -6,9 +6,7 @@ Authors: Sebastian Ullrich, Leonardo de Moura, Mario Carneiro
 module
 
 prelude
-public import Init.Control.Lawful.Basic
-public import Init.Control.Lawful.Instances
-public import Init.Control.Lawful.Lemmas
-public import Init.Control.Lawful.MonadLift
-
-public section
+import Init.Control.Lawful.Basic
+import Init.Control.Lawful.Instances
+import Init.Control.Lawful.Lemmas
+import Init.Control.Lawful.MonadLift

src/Init/Control/Lawful/Basic.lean

@@ -6,11 +6,9 @@ Authors: Sebastian Ullrich, Leonardo de Moura, Mario Carneiro
 module
 
 prelude
-public import Init.Ext
-public import Init.SimpLemmas
-public import Init.Meta
-
-public section
+import Init.Ext
+import Init.SimpLemmas
+import Init.Meta
 
 open Function
 

src/Init/Control/Lawful/Instances.lean

@@ -6,13 +6,11 @@ Authors: Sebastian Ullrich, Leonardo de Moura, Mario Carneiro
 module
 
 prelude
-public import Init.Control.Lawful.Basic
-public import all Init.Control.Except
-public import all Init.Control.State
-public import Init.Control.StateRef
-public import Init.Ext
-
-public section
+import Init.Control.Lawful.Basic
+import all Init.Control.Except
+import all Init.Control.State
+import Init.Control.StateRef
+import Init.Ext
 
 open Function
 

src/Init/Control/Lawful/Lemmas.lean

@@ -6,11 +6,9 @@ Authors: Kim Morrison
 module
 
 prelude
-public import Init.Control.Lawful.Basic
-public import Init.RCases
-public import Init.ByCases
-
-public section
+import Init.Control.Lawful.Basic
+import Init.RCases
+import Init.ByCases
 
 -- Mapping by a function with a left inverse is injective.
 theorem map_inj_of_left_inverse [Functor m] [LawfulFunctor m] {f : α → β}

src/Init/Control/Lawful/MonadLift.lean

@@ -6,8 +6,6 @@ Authors: Paul Reichert
 module
 
 prelude
-public import Init.Control.Lawful.MonadLift.Basic
-public import Init.Control.Lawful.MonadLift.Lemmas
-public import Init.Control.Lawful.MonadLift.Instances
-
-public section
+import Init.Control.Lawful.MonadLift.Basic
+import Init.Control.Lawful.MonadLift.Lemmas
+import Init.Control.Lawful.MonadLift.Instances

src/Init/Control/Lawful/MonadLift/Basic.lean

@@ -6,9 +6,7 @@ Authors: Quang Dao
 module
 
 prelude
-public import Init.Control.Basic
-
-public section
+import Init.Control.Basic
 
 /-!
 # LawfulMonadLift and LawfulMonadLiftT

src/Init/Control/Lawful/MonadLift/Instances.lean

@@ -6,16 +6,13 @@ Authors: Quang Dao, Paul Reichert
 module
 
 prelude
-public import all Init.Control.Option
-public import all Init.Control.Except
-public import all Init.Control.ExceptCps
-public import all Init.Control.StateRef
-public import all Init.Control.StateCps
-public import all Init.Control.Id
-public import Init.Control.Lawful.MonadLift.Lemmas
-public import Init.Control.Lawful.Instances
-
-public section
+import all Init.Control.Option
+import all Init.Control.Except
+import all Init.Control.ExceptCps
+import all Init.Control.StateRef
+import all Init.Control.StateCps
+import Init.Control.Lawful.MonadLift.Lemmas
+import Init.Control.Lawful.Instances
 
 universe u v w x
 
@@ -138,11 +135,3 @@ instance {ε : Type u} [Monad m] [LawfulMonad m] : LawfulMonadLift m (ExceptCpsT
     simp only [bind_assoc]
 
 end ExceptCpsT
-
-namespace Id
-
-instance [Monad m] [LawfulMonad m] : LawfulMonadLiftT Id m where
-  monadLift_pure a := by simp [monadLift]
-  monadLift_bind a f := by simp [monadLift]
-
-end Id

src/Init/Control/Lawful/MonadLift/Lemmas.lean

@@ -6,10 +6,8 @@ Authors: Quang Dao
 module
 
 prelude
-public import Init.Control.Lawful.Basic
-public import Init.Control.Lawful.MonadLift.Basic
-
-public section
+import Init.Control.Lawful.Basic
+import Init.Control.Lawful.MonadLift.Basic
 
 universe u v w
 

src/Init/Control/Option.lean

@@ -6,11 +6,9 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 module
 
 prelude
-public import Init.Data.Option.Basic
-public import Init.Control.Basic
-public import Init.Control.Except
-
-public section
+import Init.Data.Option.Basic
+import Init.Control.Basic
+import Init.Control.Except
 
 set_option linter.missingDocs true
 

src/Init/Control/Reader.lean

@@ -8,11 +8,9 @@ The Reader monad transformer for passing immutable State.
 module
 
 prelude
-public import Init.Control.Basic
-public import Init.Control.Id
-public import Init.Control.Except
-
-public section
+import Init.Control.Basic
+import Init.Control.Id
+import Init.Control.Except
 
 set_option linter.missingDocs true
 
@@ -52,4 +50,4 @@ instance ReaderT.tryFinally [MonadFinally m] : MonadFinally (ReaderT ρ m) where
 A monad with access to a read-only value of type `ρ`. The value can be locally overridden by
 `withReader`, but it cannot be mutated.
 -/
-abbrev ReaderM (ρ : Type u) := ReaderT ρ Id
+@[reducible] def ReaderM (ρ : Type u) := ReaderT ρ Id

src/Init/Control/State.lean

@@ -8,11 +8,9 @@ The State monad transformer.
 module
 
 prelude
-public import Init.Control.Basic
-public import Init.Control.Id
-public import Init.Control.Except
-
-public section
+import Init.Control.Basic
+import Init.Control.Id
+import Init.Control.Except
 
 set_option linter.missingDocs true
 

src/Init/Control/StateCps.lean

@@ -6,9 +6,7 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Init.Control.Lawful.Basic
-
-public section
+import Init.Control.Lawful.Basic
 
 set_option linter.missingDocs true
 

src/Init/Control/StateRef.lean

@@ -8,9 +8,7 @@ The State monad transformer using IO references.
 module
 
 prelude
-public import Init.System.ST
-
-public section
+import Init.System.ST
 
 set_option linter.missingDocs true
 

src/Init/Conv.lean

@@ -8,10 +8,8 @@ Notation for operators defined at Prelude.lean
 module
 
 prelude
-public import Init.Tactics
-public meta import Init.Meta
-
-public section
+import Init.Tactics
+meta import Init.Meta
 
 namespace Lean.Parser.Tactic.Conv
 
@@ -187,9 +185,6 @@ match [a, b] with
 simplifies to `a`. -/
 syntax (name := simpMatch) "simp_match" : conv
 
-/-- Removes one or more hypotheses from the local context. -/
-syntax (name := clear) "clear" (ppSpace colGt term:max)+ : conv
-
 /-- Executes the given tactic block without converting `conv` goal into a regular goal. -/
 syntax (name := nestedTacticCore) "tactic'" " => " tacticSeq : conv
 
@@ -265,7 +260,7 @@ resulting in `t'`, which becomes the new target subgoal. -/
 syntax (name := convConvSeq) "conv" " => " convSeq : conv
 
 /-- `· conv` focuses on the main conv goal and tries to solve it using `s`. -/
-macro dot:patternIgnore("· " <|> ". ") s:convSeq : conv => `(conv| {%$dot ($s) })
+macro dot:patternIgnore("·" <|> ".") s:convSeq : conv => `(conv| {%$dot ($s) })
 
 
 /-- `fail_if_success t` fails if the tactic `t` succeeds. -/
@@ -326,7 +321,7 @@ macro_rules
   | `(conv| repeat $seq) => `(conv| first | ($seq); repeat $seq | skip)
 
 /--
-Extracts `let` and `have` expressions from within the target expression.
+Extracts `let` and `let_fun` expressions from within the target expression.
 This is the conv mode version of the `extract_lets` tactic.
 
 - `extract_lets` extracts all the lets from the target.
@@ -339,17 +334,11 @@ See also `lift_lets`, which does not extract lets as local declarations.
 syntax (name := extractLets) "extract_lets " optConfig (ppSpace colGt (ident <|> hole))* : conv
 
 /--
-Lifts `let` and `have` expressions within the target expression as far out as possible.
+Lifts `let` and `let_fun` expressions within the target expression as far out as possible.
 This is the conv mode version of the `lift_lets` tactic.
 -/
 syntax (name := liftLets) "lift_lets " optConfig : conv
 
-/--
-Transforms `let` expressions into `have` expressions within the target expression when possible.
-This is the conv mode version of the `let_to_have` tactic.
--/
-syntax (name := letToHave) "let_to_have" : conv
-
 /--
 `conv => ...` allows the user to perform targeted rewriting on a goal or hypothesis,
 by focusing on particular subexpressions.

src/Init/Core.lean

@@ -8,10 +8,8 @@ notation, basic datatypes and type classes
 module
 
 prelude
-public meta import Init.Prelude
-public import Init.SizeOf
-
-public section
+meta import Init.Prelude
+import Init.SizeOf
 set_option linter.missingDocs true -- keep it documented
 
 @[expose] section
@@ -29,29 +27,6 @@ theorem id_def {α : Sort u} (a : α) : id a = a := rfl
 
 attribute [grind] id
 
-/--
-A helper gadget for instructing the kernel to eagerly reduce terms.
-
-When the gadget wraps the argument of an application, then when checking that
-the expected and inferred type of the argument match, the kernel will evaluate terms more eagerly.
-It is often used to wrap `Eq.refl true` proof terms as `eagerReduce (Eq.refl true)`
-when using proof by reflection.
-As an example, consider the theorem:
-```
-theorem eq_norm (ctx : Context) (p₁ p₂ : Poly) (h : (p₁.norm == p₂) = true) :
-  p₁.denote ctx = 0 → p₂.denote ctx = 0
-```
-The argument `h : (p₁.norm == p₂) = true` is a candidate for `eagerReduce`.
-When applying this theorem, we would write:
-
-```
-eq_norm ctx p q (eagerReduce (Eq.refl true)) h
-```
-to instruct the kernel to use eager reduction when establishing that `(p.norm == q) = true` is
-definitionally equal to `true = true`.
--/
-@[expose] def eagerReduce {α : Sort u} (a : α) : α := a
-
 /--
 `flip f a b` is `f b a`. It is useful for "point-free" programming,
 since it can sometimes be used to avoid introducing variables.
@@ -775,8 +750,6 @@ Unlike `x ≠ y` (which is notation for `Ne x y`), this is `Bool` valued instead
 
 @[inherit_doc] infix:50 " != " => bne
 
-macro_rules | `($x != $y) => `(binrel_no_prop% bne $x $y)
-
 recommended_spelling "bne" for "!=" in [bne, «term_!=_»]
 
 /-- `ReflBEq α` says that the `BEq` implementation is reflexive. -/
@@ -878,8 +851,6 @@ and asserts that `a` and `b` are not equal.
 
 @[inherit_doc] infix:50 " ≠ "  => Ne
 
-macro_rules | `($x ≠ $y) => `(binrel% Ne $x $y)
-
 recommended_spelling "ne" for "≠" in [Ne, «term_≠_»]
 
 section Ne
@@ -1559,13 +1530,38 @@ end Setoid
 /-! # Propositional extensionality -/
 
 /--
-The [axiom](lean-manual://section/axioms) of **propositional extensionality**. It asserts that if
-propositions `a` and `b` are logically equivalent (that is, if `a` can be proved from `b` and vice
-versa), then `a` and `b` are *equal*, meaning `a` can be replaced with `b` in all contexts.
+The axiom of **propositional extensionality**. It asserts that if propositions
+`a` and `b` are logically equivalent (i.e. we can prove `a` from `b` and vice versa),
+then `a` and `b` are *equal*, meaning that we can replace `a` with `b` in all
+contexts.
 
-The standard logical connectives provably respect propositional extensionality. However, an axiom is
-needed for higher order expressions like `P a` where `P : Prop → Prop` is unknown, as well as for
-equality. Propositional extensionality is intuitionistically valid.
+For simple expressions like `a ∧ c ∨ d → e` we can prove that because all the logical
+connectives respect logical equivalence, we can replace `a` with `b` in this expression
+without using `propext`. However, for higher order expressions like `P a` where
+`P : Prop → Prop` is unknown, or indeed for `a = b` itself, we cannot replace `a` with `b`
+without an axiom which says exactly this.
+
+This is a relatively uncontroversial axiom, which is intuitionistically valid.
+It does however block computation when using `#reduce` to reduce proofs directly
+(which is not recommended), meaning that canonicity,
+the property that all closed terms of type `Nat` normalize to numerals,
+fails to hold when this (or any) axiom is used:
+```
+set_option pp.proofs true
+
+def foo : Nat := by
+  have : (True → True) ↔ True := ⟨λ _ => trivial, λ _ _ => trivial⟩
+  have := propext this ▸ (2 : Nat)
+  exact this
+
+#reduce foo
+-- propext { mp := fun x x => True.intro, mpr := fun x => True.intro } ▸ 2
+
+#eval foo -- 2
+```
+`#eval` can evaluate it to a numeral because the compiler erases casts and
+does not evaluate proofs, so `propext`, whose return type is a proposition,
+can never block it.
 -/
 axiom propext {a b : Prop} : (a ↔ b) → a = b
 
@@ -1596,7 +1592,6 @@ gen_injective_theorems% MProd
 gen_injective_theorems% NonScalar
 gen_injective_theorems% Option
 gen_injective_theorems% PLift
-gen_injective_theorems% PULift
 gen_injective_theorems% PNonScalar
 gen_injective_theorems% PProd
 gen_injective_theorems% Prod
@@ -2541,7 +2536,3 @@ class Irrefl (r : α → α → Prop) : Prop where
   irrefl : ∀ a, ¬r a a
 
 end Std
-
-/-- Deprecated alias for `XorOp`. -/
-@[deprecated XorOp (since := "2025-07-30")]
-abbrev Xor := XorOp

src/Init/Data.lean

@@ -6,49 +6,44 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Init.Data.Basic
-public import Init.Data.Nat
-public import Init.Data.Bool
-public import Init.Data.BitVec
-public import Init.Data.Cast
-public import Init.Data.Char
-public import Init.Data.String
-public import Init.Data.List
-public import Init.Data.Int
-public import Init.Data.Array
-public import Init.Data.Array.Subarray.Split
-public import Init.Data.ByteArray
-public import Init.Data.FloatArray
-public import Init.Data.Fin
-public import Init.Data.UInt
-public import Init.Data.SInt
-public import Init.Data.Float
-public import Init.Data.Float32
-public import Init.Data.Option
-public import Init.Data.Ord
-public import Init.Data.Random
-public import Init.Data.ToString
-public import Init.Data.Range
-public import Init.Data.Hashable
-public import Init.Data.OfScientific
-public import Init.Data.Format
-public import Init.Data.Stream
-public import Init.Data.Prod
-public import Init.Data.AC
-public import Init.Data.Queue
-public import Init.Data.Sum
-public import Init.Data.BEq
-public import Init.Data.Subtype
-public import Init.Data.ULift
-public import Init.Data.PLift
-public import Init.Data.Zero
-public import Init.Data.NeZero
-public import Init.Data.Function
-public import Init.Data.RArray
-public import Init.Data.Vector
-public import Init.Data.Iterators
-public import Init.Data.Range.Polymorphic
-public import Init.Data.Slice
-public import Init.Data.Order
-
-public section
+import Init.Data.Basic
+import Init.Data.Nat
+import Init.Data.Bool
+import Init.Data.BitVec
+import Init.Data.Cast
+import Init.Data.Char
+import Init.Data.String
+import Init.Data.List
+import Init.Data.Int
+import Init.Data.Array
+import Init.Data.Array.Subarray.Split
+import Init.Data.ByteArray
+import Init.Data.FloatArray
+import Init.Data.Fin
+import Init.Data.UInt
+import Init.Data.SInt
+import Init.Data.Float
+import Init.Data.Float32
+import Init.Data.Option
+import Init.Data.Ord
+import Init.Data.Random
+import Init.Data.ToString
+import Init.Data.Range
+import Init.Data.Hashable
+import Init.Data.OfScientific
+import Init.Data.Format
+import Init.Data.Stream
+import Init.Data.Prod
+import Init.Data.AC
+import Init.Data.Queue
+import Init.Data.Sum
+import Init.Data.BEq
+import Init.Data.Subtype
+import Init.Data.ULift
+import Init.Data.PLift
+import Init.Data.Zero
+import Init.Data.NeZero
+import Init.Data.Function
+import Init.Data.RArray
+import Init.Data.Vector
+import Init.Data.Iterators

src/Init/Data/AC.lean

@@ -7,10 +7,8 @@ Authors: Dany Fabian
 module
 
 prelude
-public import Init.Classical
-public import Init.ByCases
-
-@[expose] public section
+import Init.Classical
+import Init.ByCases
 
 namespace Lean.Data.AC
 inductive Expr

src/Init/Data/Array.lean

@@ -6,29 +6,27 @@ Authors: Gabriel Ebner
 module
 
 prelude
-public import Init.Data.Array.Basic
-public import Init.Data.Array.QSort
-public import Init.Data.Array.BinSearch
-public import Init.Data.Array.InsertionSort
-public import Init.Data.Array.DecidableEq
-public import Init.Data.Array.Mem
-public import Init.Data.Array.Attach
-public import Init.Data.Array.BasicAux
-public import Init.Data.Array.Lemmas
-public import Init.Data.Array.TakeDrop
-public import Init.Data.Array.Bootstrap
-public import Init.Data.Array.GetLit
-public import Init.Data.Array.MapIdx
-public import Init.Data.Array.Set
-public import Init.Data.Array.Monadic
-public import Init.Data.Array.FinRange
-public import Init.Data.Array.Perm
-public import Init.Data.Array.Find
-public import Init.Data.Array.Lex
-public import Init.Data.Array.Range
-public import Init.Data.Array.Erase
-public import Init.Data.Array.Zip
-public import Init.Data.Array.InsertIdx
-public import Init.Data.Array.Extract
-
-public section
+import Init.Data.Array.Basic
+import Init.Data.Array.QSort
+import Init.Data.Array.BinSearch
+import Init.Data.Array.InsertionSort
+import Init.Data.Array.DecidableEq
+import Init.Data.Array.Mem
+import Init.Data.Array.Attach
+import Init.Data.Array.BasicAux
+import Init.Data.Array.Lemmas
+import Init.Data.Array.TakeDrop
+import Init.Data.Array.Bootstrap
+import Init.Data.Array.GetLit
+import Init.Data.Array.MapIdx
+import Init.Data.Array.Set
+import Init.Data.Array.Monadic
+import Init.Data.Array.FinRange
+import Init.Data.Array.Perm
+import Init.Data.Array.Find
+import Init.Data.Array.Lex
+import Init.Data.Array.Range
+import Init.Data.Array.Erase
+import Init.Data.Array.Zip
+import Init.Data.Array.InsertIdx
+import Init.Data.Array.Extract

src/Init/Data/Array/Attach.lean

@@ -6,12 +6,10 @@ Authors: Joachim Breitner, Mario Carneiro
 module
 
 prelude
-public import Init.Data.Array.Mem
-public import Init.Data.Array.Lemmas
-public import Init.Data.Array.Count
-public import all Init.Data.List.Attach
-
-public section
+import Init.Data.Array.Mem
+import Init.Data.Array.Lemmas
+import Init.Data.Array.Count
+import all Init.Data.List.Attach
 
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 set_option linter.indexVariables true -- Enforce naming conventions for index variables.

src/Init/Data/Array/Basic.lean

@@ -6,17 +6,15 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Init.WFTactics
-public import Init.Data.Nat.Basic
-public import Init.Data.Fin.Basic
-public import Init.Data.UInt.BasicAux
-public import Init.Data.Repr
-public import Init.Data.ToString.Basic
-public import Init.GetElem
-public import all Init.Data.List.ToArrayImpl
-public import all Init.Data.Array.Set
-
-public section
+import Init.WFTactics
+import Init.Data.Nat.Basic
+import Init.Data.Fin.Basic
+import Init.Data.UInt.BasicAux
+import Init.Data.Repr
+import Init.Data.ToString.Basic
+import Init.GetElem
+import all Init.Data.List.ToArrayImpl
+import all Init.Data.Array.Set
 
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 set_option linter.indexVariables true -- Enforce naming conventions for index variables.
@@ -180,7 +178,7 @@ in-place when the reference to the array is unique.
 
 This avoids overhead due to unboxing a `Nat` used as an index.
 -/
-@[extern "lean_array_uset", expose]
+@[extern "lean_array_uset"]
 def uset (xs : Array α) (i : USize) (v : α) (h : i.toNat < xs.size) : Array α :=
   xs.set i.toNat v h
 
@@ -263,7 +261,7 @@ Examples:
 * `#["red", "green", "blue", "brown"].swapIfInBounds 0 4 = #["red", "green", "blue", "brown"]`
 * `#["red", "green", "blue", "brown"].swapIfInBounds 9 2 = #["red", "green", "blue", "brown"]`
 -/
-@[extern "lean_array_swap", grind]
+@[extern "lean_array_swap"]
 def swapIfInBounds (xs : Array α) (i j : @& Nat) : Array α :=
   if h₁ : i < xs.size then
   if h₂ : j < xs.size then swap xs i j
@@ -1024,7 +1022,7 @@ The optional parameters `start` and `stop` control the region of the array to wh
 applied. Iteration proceeds from `start` (inclusive) to `stop` (exclusive), so `f` is not invoked
 unless `start < stop`. By default, the entire array is used.
 -/
-@[inline, expose]
+@[inline]
 protected def forM {α : Type u} {m : Type v → Type w} [Monad m] (f : α → m PUnit) (as : Array α) (start := 0) (stop := as.size) : m PUnit :=
   as.foldlM (fun _ => f) ⟨⟩ start stop
 
@@ -1165,7 +1163,7 @@ Examples:
 def zipIdx (xs : Array α) (start := 0) : Array (α × Nat) :=
   xs.mapIdx fun i a => (a, start + i)
 
-
+@[deprecated zipIdx (since := "2025-01-21")] abbrev zipWithIndex := @zipIdx
 
 /--
 Returns the first element of the array for which the predicate `p` returns `true`, or `none` if no
@@ -1285,7 +1283,7 @@ def findFinIdx? {α : Type u} (p : α → Bool) (as : Array α) : Option (Fin as
     decreasing_by simp_wf; decreasing_trivial_pre_omega
   loop 0
 
-private theorem findIdx?_loop_eq_map_findFinIdx?_loop_val {xs : Array α} {p : α → Bool} {j} :
+theorem findIdx?_loop_eq_map_findFinIdx?_loop_val {xs : Array α} {p : α → Bool} {j} :
     findIdx?.loop p xs j = (findFinIdx?.loop p xs j).map (·.val) := by
   unfold findIdx?.loop
   unfold findFinIdx?.loop
@@ -1322,7 +1320,8 @@ def idxOfAux [BEq α] (xs : Array α) (v : α) (i : Nat) : Option (Fin xs.size)
   else none
 decreasing_by simp_wf; decreasing_trivial_pre_omega
 
-
+@[deprecated idxOfAux (since := "2025-01-29")]
+abbrev indexOfAux := @idxOfAux
 
 /--
 Returns the index of the first element equal to `a`, or the size of the array if no element is equal
@@ -1337,7 +1336,8 @@ Examples:
 def finIdxOf? [BEq α] (xs : Array α) (v : α) : Option (Fin xs.size) :=
   idxOfAux xs v 0
 
-
+@[deprecated "`Array.indexOf?` has been deprecated, use `idxOf?` or `finIdxOf?` instead." (since := "2025-01-29")]
+abbrev indexOf? := @finIdxOf?
 
 /--
 Returns the index of the first element equal to `a`, or the size of the array if no element is equal
@@ -1806,7 +1806,6 @@ Examples:
 * `#["apple", "pear", "orange"].eraseIdxIfInBounds 3 = #["apple", "pear", "orange"]`
 * `#["apple", "pear", "orange"].eraseIdxIfInBounds 5 = #["apple", "pear", "orange"]`
 -/
-@[grind]
 def eraseIdxIfInBounds (xs : Array α) (i : Nat) : Array α :=
   if h : i < xs.size then xs.eraseIdx i h else xs
 
@@ -1917,7 +1916,6 @@ Examples:
  * `#["tues", "thur", "sat"].insertIdxIfInBounds 3 "wed" = #["tues", "thur", "sat", "wed"]`
  * `#["tues", "thur", "sat"].insertIdxIfInBounds 4 "wed" = #["tues", "thur", "sat"]`
 -/
-@[grind]
 def insertIdxIfInBounds (as : Array α) (i : Nat) (a : α) : Array α :=
   if h : i ≤ as.size then
     insertIdx as i a
@@ -1954,16 +1952,16 @@ def isPrefixOf [BEq α] (as bs : Array α) : Bool :=
     false
 
 @[semireducible, specialize] -- This is otherwise irreducible because it uses well-founded recursion.
-def zipWithMAux {m : Type v → Type w} [Monad m] (as : Array α) (bs : Array β) (f : α → β → m γ) (i : Nat) (cs : Array γ) : m (Array γ) := do
+def zipWithAux (as : Array α) (bs : Array β) (f : α → β → γ) (i : Nat) (cs : Array γ) : Array γ :=
   if h : i < as.size then
     let a := as[i]
     if h : i < bs.size then
       let b := bs[i]
-      zipWithMAux as bs f (i+1) <| cs.push (← f a b)
+      zipWithAux as bs f (i+1) <| cs.push <| f a b
     else
-      return cs
+      cs
   else
-    return cs
+    cs
 decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 /--
@@ -1977,7 +1975,7 @@ Examples:
 * `#[x₁, x₂, x₃].zipWith f #[y₁, y₂, y₃, y₄] = #[f x₁ y₁, f x₂ y₂, f x₃ y₃]`
 -/
 @[inline] def zipWith (f : α → β → γ) (as : Array α) (bs : Array β) : Array γ :=
-  Id.run (zipWithMAux as bs (pure <| f · ·) 0 #[])
+  zipWithAux as bs f 0 #[]
 
 /--
 Combines two arrays into an array of pairs in which the first and second components are the
@@ -2014,13 +2012,6 @@ where go (as : Array α) (bs : Array β) (i : Nat) (cs : Array γ) :=
   termination_by max as.size bs.size - i
   decreasing_by simp_wf; decreasing_trivial_pre_omega
 
-/--
-Applies a monadic function to the corresponding elements of two arrays, left-to-right, stopping at
-the end of the shorter array. `zipWithM f as bs` is equivalent to `mapM id (zipWith f as bs)`.
--/
-@[inline] def zipWithM {m : Type v → Type w} [Monad m] (f : α → β → m γ) (as : Array α) (bs : Array β) : m (Array γ) :=
-  zipWithMAux as bs f 0 #[]
-
 /--
 Separates an array of pairs into two arrays that contain the respective first and second components.
 

src/Init/Data/Array/BasicAux.lean

@@ -6,11 +6,9 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import all Init.Data.Array.Basic
-public import Init.Data.Nat.Linear
-public import Init.NotationExtra
-
-public section
+import all Init.Data.Array.Basic
+import Init.Data.Nat.Linear
+import Init.NotationExtra
 
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 set_option linter.indexVariables true -- Enforce naming conventions for index variables.

src/Init/Data/Array/BinSearch.lean

@@ -6,11 +6,9 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Init.Data.Array.Basic
-public import Init.Data.Int.DivMod.Lemmas
-public import Init.Omega
-
-public section
+import Init.Data.Array.Basic
+import Init.Data.Int.DivMod.Lemmas
+import Init.Omega
 universe u v
 
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.

src/Init/Data/Array/Bootstrap.lean

@@ -7,10 +7,8 @@ Authors: Mario Carneiro
 module
 
 prelude
-public import Init.Data.List.TakeDrop
-public import all Init.Data.Array.Basic
-
-public section
+import Init.Data.List.TakeDrop
+import all Init.Data.Array.Basic
 
 /-!
 ## Bootstrapping theorems about arrays
@@ -123,9 +121,15 @@ abbrev pop_toList := @Array.toList_pop
 @[simp, grind =] theorem append_empty {xs : Array α} : xs ++ #[] = xs := by
   apply ext'; simp only [toList_append, List.append_nil]
 
+@[deprecated append_empty (since := "2025-01-13")]
+abbrev append_nil := @append_empty
+
 @[simp, grind =] theorem empty_append {xs : Array α} : #[] ++ xs = xs := by
   apply ext'; simp only [toList_append, List.nil_append]
 
+@[deprecated empty_append (since := "2025-01-13")]
+abbrev nil_append := @empty_append
+
 @[simp, grind _=_] theorem append_assoc {xs ys zs : Array α} : xs ++ ys ++ zs = xs ++ (ys ++ zs) := by
   apply ext'; simp only [toList_append, List.append_assoc]
 
@@ -136,6 +140,7 @@ abbrev pop_toList := @Array.toList_pop
   rw [← appendList_eq_append]; unfold Array.appendList
   induction l generalizing xs <;> simp [*]
 
-
+@[deprecated toList_appendList (since := "2024-12-11")]
+abbrev appendList_toList := @toList_appendList
 
 end Array

src/Init/Data/Array/Count.lean

@@ -6,11 +6,9 @@ Authors: Kim Morrison
 module
 
 prelude
-public import all Init.Data.Array.Basic
-public import Init.Data.Array.Lemmas
-public import Init.Data.List.Nat.Count
-
-public section
+import all Init.Data.Array.Basic
+import Init.Data.Array.Lemmas
+import Init.Data.List.Nat.Count
 
 /-!
 # Lemmas about `Array.countP` and `Array.count`.

src/Init/Data/Array/DecidableEq.lean

@@ -6,12 +6,10 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import all Init.Data.Array.Basic
-public import Init.Data.BEq
-public import Init.Data.List.Nat.BEq
-public import Init.ByCases
-
-public section
+import all Init.Data.Array.Basic
+import Init.Data.BEq
+import Init.Data.List.Nat.BEq
+import Init.ByCases
 
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 set_option linter.indexVariables true -- Enforce naming conventions for index variables.

src/Init/Data/Array/Erase.lean

@@ -6,12 +6,10 @@ Authors: Kim Morrison
 module
 
 prelude
-public import all Init.Data.Array.Basic
-public import Init.Data.Array.Lemmas
-public import Init.Data.List.Nat.Erase
-public import Init.Data.List.Nat.Basic
-
-public section
+import all Init.Data.Array.Basic
+import Init.Data.Array.Lemmas
+import Init.Data.List.Nat.Erase
+import Init.Data.List.Nat.Basic
 
 /-!
 # Lemmas about `Array.eraseP`, `Array.erase`, and `Array.eraseIdx`.
@@ -382,12 +380,11 @@ theorem eraseIdx_ne_empty_iff {xs : Array α} {i : Nat} {h} : xs.eraseIdx i ≠
     simp [h]
   · simp
 
+@[grind →]
 theorem mem_of_mem_eraseIdx {xs : Array α} {i : Nat} {h} {a : α} (h : a ∈ xs.eraseIdx i) : a ∈ xs := by
   rcases xs with ⟨xs⟩
   simpa using List.mem_of_mem_eraseIdx (by simpa using h)
 
-grind_pattern mem_of_mem_eraseIdx => a ∈ xs.eraseIdx i
-
 theorem eraseIdx_append_of_lt_size {xs : Array α} {k : Nat} (hk : k < xs.size) (ys : Array α) (h) :
     eraseIdx (xs ++ ys) k = eraseIdx xs k ++ ys := by
   rcases xs with ⟨l⟩

src/Init/Data/Array/Extract.lean

@@ -6,10 +6,8 @@ Authors: Kim Morrison
 module
 
 prelude
-public import Init.Data.Array.Lemmas
-public import Init.Data.List.Nat.TakeDrop
-
-public section
+import Init.Data.Array.Lemmas
+import Init.Data.List.Nat.TakeDrop
 
 /-!
 # Lemmas about `Array.extract`
@@ -48,45 +46,15 @@ theorem size_extract_of_le {as : Array α} {i j : Nat} (h : j ≤ as.size) :
   simp
   omega
 
-@[grind =]
-theorem extract_push {as : Array α} {b : α} {start stop : Nat} :
-    (as.push b).extract start stop =
-      if stop ≤ as.size then
-        as.extract start stop
-      else if start ≤ as.size then
-        (as.extract start as.size).push b
-      else #[] := by
-  split
-  · ext i h₁ h₂
-    · simp
-      omega
-    · simp only [size_extract, size_push] at h₁ h₂
-      simp only [getElem_extract, getElem_push]
-      rw [dif_pos (by omega)]
-  · split
-    · ext i h₁ h₂
-      · simp
-        omega
-      · simp only [size_extract, size_push] at h₁ h₂
-        simp only [getElem_extract, getElem_push]
-        split <;> rename_i h₃
-        · split
-          · rfl
-          · simp_all
-            omega
-        · split <;> rename_i h₄
-          · simp at h₄
-            omega
-          · rfl
-    · ext i h₁ h₂
-      · simp
-        omega
-      · simp at h₂
-
-@[simp]
-theorem extract_push_of_le {as : Array α} {b : α} {start stop : Nat} (h : stop ≤ as.size) :
+@[simp, grind =]
+theorem extract_push {as : Array α} {b : α} {start stop : Nat} (h : stop ≤ as.size) :
     (as.push b).extract start stop = as.extract start stop := by
-  rw [extract_push, if_pos h]
+  ext i h₁ h₂
+  · simp
+    omega
+  · simp only [size_extract, size_push] at h₁ h₂
+    simp only [getElem_extract, getElem_push]
+    rw [dif_pos (by omega)]
 
 @[simp, grind =]
 theorem extract_eq_pop {as : Array α} {stop : Nat} (h : stop = as.size - 1) :

src/Init/Data/Array/FinRange.lean

@@ -6,10 +6,8 @@ Authors: François G. Dorais
 module
 
 prelude
-public import Init.Data.List.FinRange
-public import Init.Data.Array.OfFn
-
-public section
+import Init.Data.List.FinRange
+import Init.Data.Array.OfFn
 
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 set_option linter.indexVariables true -- Enforce naming conventions for index variables.

src/Init/Data/Array/Find.lean

@@ -6,13 +6,11 @@ Authors: Kim Morrison
 module
 
 prelude
-public import Init.Data.List.Nat.Find
-public import all Init.Data.Array.Basic
-public import Init.Data.Array.Lemmas
-public import Init.Data.Array.Attach
-public import Init.Data.Array.Range
-
-public section
+import Init.Data.List.Nat.Find
+import all Init.Data.Array.Basic
+import Init.Data.Array.Lemmas
+import Init.Data.Array.Attach
+import Init.Data.Array.Range
 
 /-!
 # Lemmas about `Array.findSome?`, `Array.find?, `Array.findIdx`, `Array.findIdx?`, `Array.idxOf`.
@@ -387,7 +385,7 @@ theorem find?_eq_some_iff_getElem {xs : Array α} {p : α → Bool} {b : α} :
 /-! ### findIdx -/
 
 @[grind =]
-theorem findIdx_empty : findIdx p #[] = 0 := by simp
+theorem findIdx_empty : findIdx p #[] = 0 := rfl
 
 @[grind =]
 theorem findIdx_singleton {a : α} {p : α → Bool} :

src/Init/Data/Array/GetLit.lean

@@ -7,9 +7,7 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Init.Data.Array.Basic
-
-public section
+import Init.Data.Array.Basic
 
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 set_option linter.indexVariables true -- Enforce naming conventions for index variables.

src/Init/Data/Array/InsertIdx.lean

@@ -6,10 +6,8 @@ Authors: Kim Morrison
 module
 
 prelude
-public import Init.Data.Array.Lemmas
-public import Init.Data.List.Nat.InsertIdx
-
-public section
+import Init.Data.Array.Lemmas
+import Init.Data.List.Nat.InsertIdx
 
 /-!
 # insertIdx

src/Init/Data/Array/InsertionSort.lean

@@ -6,9 +6,7 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Init.Data.Array.Basic
-
-public section
+import Init.Data.Array.Basic
 
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 set_option linter.indexVariables true -- Enforce naming conventions for index variables.

src/Init/Data/Array/Lemmas.lean

@@ -6,24 +6,21 @@ Authors: Mario Carneiro, Kim Morrison
 module
 
 prelude
-public import Init.Data.Nat.Lemmas
-public import Init.Data.List.Range
-public import Init.Data.List.Nat.TakeDrop
-public import Init.Data.List.Nat.Modify
-public import Init.Data.List.Nat.Basic
-public import Init.Data.List.Monadic
-public import Init.Data.List.OfFn
-public import Init.Data.Array.Mem
-public import Init.Data.Array.DecidableEq
-public import Init.Data.Array.Lex.Basic
-public import Init.Data.Range.Lemmas
-public import Init.TacticsExtra
-public import Init.Data.List.ToArray
+import Init.Data.Nat.Lemmas
+import Init.Data.List.Range
 import all Init.Data.List.Control
-import all Init.Data.Array.Basic
+import Init.Data.List.Nat.TakeDrop
+import Init.Data.List.Nat.Modify
+import Init.Data.List.Nat.Basic
+import Init.Data.List.Monadic
+import Init.Data.List.OfFn
 import all Init.Data.Array.Bootstrap
-
-public section
+import Init.Data.Array.Mem
+import Init.Data.Array.DecidableEq
+import Init.Data.Array.Lex.Basic
+import Init.Data.Range.Lemmas
+import Init.TacticsExtra
+import Init.Data.List.ToArray
 
 /-!
 ## Theorems about `Array`.
@@ -130,7 +127,7 @@ theorem none_eq_getElem?_iff {xs : Array α} {i : Nat} : none = xs[i]? ↔ xs.si
 theorem getElem?_eq_none {xs : Array α} (h : xs.size ≤ i) : xs[i]? = none := by
   simp [h]
 
-grind_pattern Array.getElem?_eq_none => xs.size, xs[i]?
+grind_pattern Array.getElem?_eq_none => xs.size ≤ i, xs[i]?
 
 @[simp] theorem getElem?_eq_getElem {xs : Array α} {i : Nat} (h : i < xs.size) : xs[i]? = some xs[i] :=
   getElem?_pos ..
@@ -838,10 +835,16 @@ theorem mem_of_contains_eq_true [BEq α] [LawfulBEq α] {a : α} {as : Array α}
   cases as
   simp
 
+@[deprecated mem_of_contains_eq_true (since := "2024-12-12")]
+abbrev mem_of_elem_eq_true := @mem_of_contains_eq_true
+
 theorem contains_eq_true_of_mem [BEq α] [LawfulBEq α] {a : α} {as : Array α} (h : a ∈ as) : as.contains a = true := by
   cases as
   simpa using h
 
+@[deprecated contains_eq_true_of_mem (since := "2024-12-12")]
+abbrev elem_eq_true_of_mem := @contains_eq_true_of_mem
+
 @[simp] theorem elem_eq_contains [BEq α] {a : α} {xs : Array α} :
     elem a xs = xs.contains a := by
   simp [elem]
@@ -867,24 +870,24 @@ theorem elem_eq_mem [BEq α] [LawfulBEq α] {a : α} {xs : Array α} :
 @[grind] theorem all_empty [BEq α] {p : α → Bool} : (#[] : Array α).all p = true := by simp
 
 /-- Variant of `any_push` with a side condition on `stop`. -/
-@[simp, grind] theorem any_push' {xs : Array α} {a : α} {p : α → Bool} (h : stop = xs.size + 1) :
+@[simp, grind] theorem any_push' [BEq α] {xs : Array α} {a : α} {p : α → Bool} (h : stop = xs.size + 1) :
     (xs.push a).any p 0 stop = (xs.any p || p a) := by
   cases xs
   rw [List.push_toArray]
   simp [h]
 
-theorem any_push {xs : Array α} {a : α} {p : α → Bool} :
+theorem any_push [BEq α] {xs : Array α} {a : α} {p : α → Bool} :
     (xs.push a).any p = (xs.any p || p a) :=
   any_push' (by simp)
 
 /-- Variant of `all_push` with a side condition on `stop`. -/
-@[simp, grind] theorem all_push' {xs : Array α} {a : α} {p : α → Bool} (h : stop = xs.size + 1) :
+@[simp, grind] theorem all_push' [BEq α] {xs : Array α} {a : α} {p : α → Bool} (h : stop = xs.size + 1) :
     (xs.push a).all p 0 stop = (xs.all p && p a) := by
   cases xs
   rw [List.push_toArray]
   simp [h]
 
-theorem all_push {xs : Array α} {a : α} {p : α → Bool} :
+theorem all_push [BEq α] {xs : Array α} {a : α} {p : α → Bool} :
     (xs.push a).all p = (xs.all p && p a) :=
   all_push' (by simp)
 
@@ -899,9 +902,15 @@ theorem all_push {xs : Array α} {a : α} {p : α → Bool} :
   cases xs
   simp
 
+@[deprecated getElem_set_self (since := "2024-12-11")]
+abbrev getElem_set_eq := @getElem_set_self
+
 @[simp] theorem getElem?_set_self {xs : Array α} {i : Nat} (h : i < xs.size) {v : α} :
     (xs.set i v)[i]? = some v := by simp [h]
 
+@[deprecated getElem?_set_self (since := "2024-12-11")]
+abbrev getElem?_set_eq := @getElem?_set_self
+
 @[simp] theorem getElem_set_ne {xs : Array α} {i : Nat} (h' : i < xs.size) {v : α} {j : Nat}
     (pj : j < xs.size) (h : i ≠ j) :
     (xs.set i v)[j]'(by simp [*]) = xs[j] := by
@@ -974,13 +983,12 @@ theorem mem_set {xs : Array α} {i : Nat} (h : i < xs.size) {a : α} :
   simp [mem_iff_getElem]
   exact ⟨i, (by simpa using h), by simp⟩
 
+@[grind →]
 theorem mem_or_eq_of_mem_set
     {xs : Array α} {i : Nat} {a b : α} {w : i < xs.size} (h : a ∈ xs.set i b) : a ∈ xs ∨ a = b := by
   cases xs
   simpa using List.mem_or_eq_of_mem_set (by simpa using h)
 
-grind_pattern mem_or_eq_of_mem_set => a ∈ xs.set i b
-
 /-! ### setIfInBounds -/
 
 @[simp, grind] theorem setIfInBounds_empty {i : Nat} {a : α} :
@@ -992,6 +1000,9 @@ grind_pattern mem_or_eq_of_mem_set => a ∈ xs.set i b
 theorem setIfInBounds_def (xs : Array α) (i : Nat) (a : α) :
     xs.setIfInBounds i a = if h : i < xs.size then xs.set i a else xs := rfl
 
+@[deprecated set!_eq_setIfInBounds (since := "2024-12-12")]
+abbrev set!_is_setIfInBounds := @set!_eq_setIfInBounds
+
 @[simp, grind] theorem size_setIfInBounds {xs : Array α} {i : Nat} {a : α} :
     (xs.setIfInBounds i a).size = xs.size := by
   if h : i < xs.size  then
@@ -1013,6 +1024,9 @@ theorem setIfInBounds_def (xs : Array α) (i : Nat) (a : α) :
   simp at h
   simp only [setIfInBounds, h, ↓reduceDIte, getElem_set_self]
 
+@[deprecated getElem_setIfInBounds_self (since := "2024-12-11")]
+abbrev getElem_setIfInBounds_eq := @getElem_setIfInBounds_self
+
 @[simp] theorem getElem_setIfInBounds_ne {xs : Array α} {i : Nat} {a : α} {j : Nat}
     (hj : j < xs.size) (h : i ≠ j) :
     (xs.setIfInBounds i a)[j]'(by simpa using hj) = xs[j] := by
@@ -1032,6 +1046,9 @@ theorem getElem?_setIfInBounds_self_of_lt {xs : Array α} {i : Nat} {a : α} (h
     (xs.setIfInBounds i a)[i]? = some a := by
   simp [h]
 
+@[deprecated getElem?_setIfInBounds_self (since := "2024-12-11")]
+abbrev getElem?_setIfInBounds_eq := @getElem?_setIfInBounds_self
+
 @[simp] theorem getElem?_setIfInBounds_ne {xs : Array α} {i j : Nat} (h : i ≠ j) {a : α}  :
     (xs.setIfInBounds i a)[j]? = xs[j]? := by
   simp [getElem?_setIfInBounds, h]
@@ -1357,6 +1374,23 @@ theorem mapM_eq_mapM_toList [Monad m] [LawfulMonad m] {f : α → m β} {xs : Ar
     toList <$> xs.mapM f = xs.toList.mapM f := by
   simp [mapM_eq_mapM_toList]
 
+@[deprecated "Use `mapM_eq_foldlM` instead" (since := "2025-01-08")]
+theorem mapM_map_eq_foldl {as : Array α} {f : α → β} {i : Nat} :
+    mapM.map (m := Id) (pure <| f ·) as i b = pure (as.foldl (start := i) (fun acc a => acc.push (f a)) b) := by
+  unfold mapM.map
+  split <;> rename_i h
+  · ext : 1
+    dsimp [foldl, foldlM]
+    rw [mapM_map_eq_foldl, dif_pos (by omega), foldlM.loop, dif_pos h]
+    -- Calling `split` here gives a bad goal.
+    have : size as - i = Nat.succ (size as - i - 1) := by omega
+    rw [this]
+    simp [foldl, foldlM, Nat.sub_add_eq]
+  · dsimp [foldl, foldlM]
+    rw [dif_pos (by omega), foldlM.loop, dif_neg h]
+    rfl
+termination_by as.size - i
+
 /--
 Use this as `induction ass using array₂_induction` on a hypothesis of the form `ass : Array (Array α)`.
 The hypothesis `ass` will be replaced with a hypothesis `ass : List (List α)`,
@@ -1639,12 +1673,12 @@ theorem filterMap_eq_map' {f : α → β} (w : stop = as.size) :
     filterMap (fun x => some (f x)) as 0 stop = map f as :=
   filterMap_eq_map w
 
-theorem filterMap_some_fun : filterMap (some : α → Option α) = id := by
+@[simp] theorem filterMap_some_fun : filterMap (some : α → Option α) = id := by
   funext xs
   cases xs
   simp
 
-@[simp, grind] theorem filterMap_some {xs : Array α} : filterMap some xs = xs := by
+@[grind] theorem filterMap_some {xs : Array α} : filterMap some xs = xs := by
   cases xs
   simp
 
@@ -2962,6 +2996,9 @@ theorem getElem?_extract {xs : Array α} {start stop : Nat} :
   · rw [size_extract, Nat.min_self, Nat.sub_zero]
   · intros; rw [getElem_extract]; congr; rw [Nat.zero_add]
 
+@[deprecated extract_size (since := "2025-01-19")]
+abbrev extract_all := @extract_size
+
 theorem extract_empty_of_stop_le_start {xs : Array α} {start stop : Nat} (h : stop ≤ start) :
     xs.extract start stop = #[] := by
   simp only [extract, Nat.sub_eq, emptyWithCapacity_eq]
@@ -2996,14 +3033,14 @@ theorem take_size {xs : Array α} : xs.take xs.size = xs := by
 
 /-! ### shrink -/
 
-@[simp] private theorem size_shrink_loop {xs : Array α} {n : Nat} : (shrink.loop n xs).size = xs.size - n := by
+@[simp] theorem size_shrink_loop {xs : Array α} {n : Nat} : (shrink.loop n xs).size = xs.size - n := by
   induction n generalizing xs with
   | zero => simp [shrink.loop]
   | succ n ih =>
     simp [shrink.loop, ih]
     omega
 
-@[simp] private theorem getElem_shrink_loop {xs : Array α} {n i : Nat} (h : i < (shrink.loop n xs).size) :
+@[simp] theorem getElem_shrink_loop {xs : Array α} {n i : Nat} (h : i < (shrink.loop n xs).size) :
     (shrink.loop n xs)[i] = xs[i]'(by simp at h; omega) := by
   induction n generalizing xs i with
   | zero => simp [shrink.loop]
@@ -3272,11 +3309,11 @@ theorem foldl_induction
   let rec go {i j b} (h₁ : j ≤ as.size) (h₂ : as.size ≤ i + j) (H : motive j b) :
     (motive as.size) (foldlM.loop (m := Id) f as as.size (Nat.le_refl _) i j b) := by
     unfold foldlM.loop; split
-    next hj =>
+    · next hj =>
       split
       · cases Nat.not_le_of_gt (by simp [hj]) h₂
       · exact go hj (by rwa [Nat.succ_add] at h₂) (hf ⟨j, hj⟩ b H)
-    next hj => exact Nat.le_antisymm h₁ (Nat.ge_of_not_lt hj) ▸ H
+    · next hj => exact Nat.le_antisymm h₁ (Nat.ge_of_not_lt hj) ▸ H
   simpa [foldl, foldlM] using go (Nat.zero_le _) (Nat.le_refl _) h0
 
 theorem foldr_induction
@@ -3286,13 +3323,13 @@ theorem foldr_induction
   let rec go {i b} (hi : i ≤ as.size) (H : motive i b) :
     (motive 0) (foldrM.fold (m := Id) f as 0 i hi b) := by
     unfold foldrM.fold; simp; split
-    next hi => exact (hi ▸ H)
-    next hi =>
+    · next hi => exact (hi ▸ H)
+    · next hi =>
       split; {simp at hi}
-      next i hi' =>
+      · next i hi' =>
         exact go _ (hf ⟨i, hi'⟩ b H)
   simp [foldr, foldrM]; split; {exact go _ h0}
-  next h => exact (Nat.eq_zero_of_not_pos h ▸ h0)
+  · next h => exact (Nat.eq_zero_of_not_pos h ▸ h0)
 
 @[congr]
 theorem foldl_congr {as bs : Array α} (h₀ : as = bs) {f g : β → α → β} (h₁ : f = g)
@@ -4279,7 +4316,7 @@ Examples:
 
 /-! ### Preliminaries about `ofFn` -/
 
-@[simp] private theorem size_ofFn_go {n} {f : Fin n → α} {i acc h} :
+@[simp] theorem size_ofFn_go {n} {f : Fin n → α} {i acc h} :
     (ofFn.go f acc i h).size = acc.size + i := by
   induction i generalizing acc with
   | zero => simp [ofFn.go]
@@ -4289,7 +4326,7 @@ Examples:
 @[simp] theorem size_ofFn {n : Nat} {f : Fin n → α} : (ofFn f).size = n := by simp [ofFn]
 
 -- Recall `ofFn.go f acc i h = acc ++ #[f (n - i), ..., f(n - 1)]`
-private theorem getElem_ofFn_go {f : Fin n → α} {acc i k} (h : i ≤ n) (w₁ : k < acc.size + i) :
+theorem getElem_ofFn_go {f : Fin n → α} {acc i k} (h : i ≤ n) (w₁ : k < acc.size + i) :
     (ofFn.go f acc i h)[k]'(by simpa using w₁) =
       if w₂ : k < acc.size then acc[k] else f ⟨n - i + k - acc.size, by omega⟩ := by
   induction i generalizing acc k with
@@ -4373,17 +4410,10 @@ theorem getElem?_range {n : Nat} {i : Nat} : (Array.range n)[i]? = if i < n then
 
 -- Without further algebraic hypotheses, there's no useful `sum_push` lemma.
 
-@[simp, grind =]
 theorem sum_eq_sum_toList [Add α] [Zero α] {as : Array α} : as.toList.sum = as.sum := by
   cases as
   simp [Array.sum, List.sum]
 
-@[simp, grind =]
-theorem sum_append_nat {as₁ as₂ : Array Nat} : (as₁ ++ as₂).sum = as₁.sum + as₂.sum := by
-  cases as₁
-  cases as₂
-  simp [List.sum_append_nat]
-
 theorem foldl_toList_eq_flatMap {l : List α} {acc : Array β}
     {F : Array β → α → Array β} {G : α → List β}
     (H : ∀ acc a, (F acc a).toList = acc.toList ++ G a) :
@@ -4694,10 +4724,27 @@ end List
 /-! ### Deprecations -/
 namespace Array
 
+@[deprecated size_toArray (since := "2024-12-11")]
+theorem size_mk (as : List α) : (Array.mk as).size = as.length := by simp
+
+@[deprecated getElem?_eq_getElem (since := "2024-12-11")]
+theorem getElem?_lt
+    (xs : Array α) {i : Nat} (h : i < xs.size) : xs[i]? = some xs[i] := dif_pos h
+
+@[deprecated getElem?_eq_none (since := "2024-12-11")]
+theorem getElem?_ge
+    (xs : Array α) {i : Nat} (h : i ≥ xs.size) : xs[i]? = none := dif_neg (Nat.not_lt_of_le h)
+
 set_option linter.deprecated false in
 @[deprecated "`get?` is deprecated" (since := "2025-02-12"), simp]
 theorem get?_eq_getElem? (xs : Array α) (i : Nat) : xs.get? i = xs[i]? := rfl
 
+@[deprecated getElem?_eq_none (since := "2024-12-11")]
+theorem getElem?_len_le (xs : Array α) {i : Nat} (h : xs.size ≤ i) : xs[i]? = none := by
+  simp [h]
+
+@[deprecated getD_getElem? (since := "2024-12-11")] abbrev getD_get? := @getD_getElem?
+
 @[deprecated getD_eq_getD_getElem? (since := "2025-02-12")] abbrev getD_eq_get? := @getD_eq_getD_getElem?
 
 set_option linter.deprecated false in
@@ -4722,9 +4769,64 @@ theorem get?_eq_get?_toList (xs : Array α) (i : Nat) : xs.get? i = xs.toList.ge
 set_option linter.deprecated false in
 @[deprecated get!_eq_getD_getElem? (since := "2025-02-12")] abbrev get!_eq_get? := @get!_eq_getD_getElem?
 
+@[deprecated getElem_set_self (since := "2025-01-17")]
+theorem get_set_eq (xs : Array α) (i : Nat) (v : α) (h : i < xs.size) :
+    (xs.set i v h)[i]'(by simp [h]) = v := by
+  simp only [set, ← getElem_toList, List.getElem_set_self]
+
+@[deprecated Array.getElem_toList (since := "2024-12-08")]
+theorem getElem_eq_getElem_toList {xs : Array α} (h : i < xs.size) : xs[i] = xs.toList[i] := rfl
+
+@[deprecated Array.getElem?_toList (since := "2024-12-08")]
+theorem getElem?_eq_getElem?_toList (xs : Array α) (i : Nat) : xs[i]? = xs.toList[i]? := by
+  rw [getElem?_def]
+  split <;> simp_all
+
+@[deprecated LawfulGetElem.getElem?_def (since := "2024-12-08")]
+theorem getElem?_eq {xs : Array α} {i : Nat} :
+    xs[i]? = if h : i < xs.size then some xs[i] else none := by
+  rw [getElem?_def]
+
+/-! ### map -/
+
+@[deprecated "Use `toList_map` or `List.map_toArray` to characterize `Array.map`." (since := "2025-01-06")]
+theorem map_induction (xs : Array α) (f : α → β) (motive : Nat → Prop) (h0 : motive 0)
+    (p : Fin xs.size → β → Prop) (hs : ∀ i, motive i.1 → p i (f xs[i]) ∧ motive (i+1)) :
+    motive xs.size ∧
+      ∃ eq : (xs.map f).size = xs.size, ∀ i h, p ⟨i, h⟩ ((xs.map f)[i]) := by
+  have t := foldl_induction (as := xs) (β := Array β)
+    (motive := fun i xs => motive i ∧ xs.size = i ∧ ∀ i h2, p i xs[i.1])
+    (init := #[]) (f := fun acc a => acc.push (f a)) ?_ ?_
+  obtain ⟨m, eq, w⟩ := t
+  · refine ⟨m, by simp, ?_⟩
+    intro i h
+    simp only [eq] at w
+    specialize w ⟨i, h⟩ h
+    simpa using w
+  · exact ⟨h0, rfl, nofun⟩
+  · intro i bs ⟨m, ⟨eq, w⟩⟩
+    refine ⟨?_, ?_, ?_⟩
+    · exact (hs _ m).2
+    · simp_all
+    · intro j h
+      simp at h ⊢
+      by_cases h' : j < size bs
+      · rw [getElem_push]
+        simp_all
+      · rw [getElem_push, dif_neg h']
+        simp only [show j = i by omega]
+        exact (hs _ m).1
+
+set_option linter.deprecated false in
+@[deprecated "Use `toList_map` or `List.map_toArray` to characterize `Array.map`." (since := "2025-01-06")]
+theorem map_spec (xs : Array α) (f : α → β) (p : Fin xs.size → β → Prop)
+    (hs : ∀ i, p i (f xs[i])) :
+    ∃ eq : (xs.map f).size = xs.size, ∀ i h, p ⟨i, h⟩ ((xs.map f)[i]) := by
+  simpa using map_induction xs f (fun _ => True) trivial p (by simp_all)
+
 /-! ### set -/
 
-@[deprecated getElem?_set_self (since := "2025-02-27")] abbrev get?_set_eq := @getElem?_set_self
+@[deprecated getElem?_set_eq (since := "2025-02-27")] abbrev get?_set_eq := @getElem?_set_self
 @[deprecated getElem?_set_ne (since := "2025-02-27")] abbrev get?_set_ne := @getElem?_set_ne
 @[deprecated getElem?_set (since := "2025-02-27")] abbrev get?_set := @getElem?_set
 @[deprecated get_set (since := "2025-02-27")] abbrev get_set := @getElem_set