doc: improve grind doc string

This PR fixes some bugs with the local Lake artifact cache and cleans up
the surrounding API. It also adds the ability to opt-in to the cache on
packages without `enableArtifactCache` set using the
`LAKE_ARTIFACT_CACHE` environment variable.

Bug-wise, this fixes an issue where cached executable did not have right
permissions to run on Unix systems and a bug where cached artifacts
would not be invalidated on changes. Lake also now writes a trace file
to local build directory if there is none when fetching an artifact from
the cache. This trace has a new `synthetic` field set to `true` to
distinguish it from traces produced by full builds.

.github/workflows/awaiting-manual.yml

@@ -0,0 +1,38 @@
+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

@@ -107,6 +107,7 @@ jobs:
             ${{ 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 }}
@@ -248,6 +249,7 @@ jobs:
             ${{ 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 }}

.github/workflows/ci.yml

@@ -145,6 +145,7 @@ 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
               {
@@ -167,11 +168,13 @@ jobs:
                 "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 developrs get PR toolchains (so secondary is sufficient)
+                // 1. To run it in PRs so developers 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)
-                "check-level": isPr ? 0 : 2,
+                // 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,
                 "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",
@@ -421,6 +424,6 @@ jobs:
           GITHUB_TOKEN: ${{ secrets.RELEASE_INDEX_TOKEN }}
       - name: Update toolchain on mathlib4's nightly-testing branch
         run: |
-          gh workflow -R leanprover-community/mathlib4 run nightly_bump_toolchain.yml
+          gh workflow -R leanprover-community/mathlib4-nightly-testing run nightly_bump_toolchain.yml
         env:
           GITHUB_TOKEN: ${{ secrets.MATHLIB4_BOT }}

.github/workflows/grove.yml

@@ -0,0 +1,161 @@
+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. Skipping for now, to be enabled later."
+              echo "should-run=false" >> "$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"
+              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.3
+        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.*
+          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.3
+        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

@@ -154,7 +154,7 @@ jobs:
         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
+      - name: Check merge-base and nightly-testing-YYYY-MM-DD for Mathlib/Batteries
         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.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")"
 
             if [[ -n "$BATTERIES_REMOTE_TAGS" ]]; then
               echo "... and Batteries has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
@@ -183,7 +183,6 @@ 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"
@@ -265,6 +264,108 @@ 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
@@ -355,7 +456,7 @@ jobs:
         if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
         uses: actions/checkout@v4
         with:
-          repository: leanprover-community/mathlib4
+          repository: leanprover-community/mathlib4-nightly-testing
           token: ${{ secrets.MATHLIB4_BOT }}
           ref: nightly-testing
           fetch-depth: 0 # This ensures we check out all tags and branches.
@@ -411,3 +512,63 @@ 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 }}

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")
+    if("${var}" MATCHES "USE_GMP|CHECK_OLEAN_VERSION|LEAN_VERSION_.*|LEAN_SPECIAL_VERSION_DESC")
       # 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")

doc/dev/ffi.md

@@ -131,14 +131,21 @@ 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,5 +85,13 @@ 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`
-that uses the toolchain for your PR, and will report back to the Lean PR with results from Mathlib CI.
+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.
 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/std/grove/.gitignore

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

doc/std/grove/GroveStdlib/Generated.lean

@@ -0,0 +1,14 @@
+import Grove.Framework
+import GroveStdlib.Generated.«associative-query-operations»
+
+/-
+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

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

@@ -0,0 +1,486 @@
+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 α} (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 α} [EquivBEq α]\n  [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} (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} (t : Std.DTreeMap.Raw α β cmp) :\n  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} (t : Std.ExtDTreeMap α β cmp) :\n  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 α} (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 α] [LawfulHashable α]\n  (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} (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} (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} (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 α] [LawfulHashable α]\n  (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 α} (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 α} [EquivBEq α]\n  [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} (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} (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} (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 α} (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 α] [LawfulHashable α]\n  (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} (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} (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} (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} (t : Std.DTreeMap α β cmp)\n  (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} (t : Std.DTreeMap.Raw α β cmp)\n  (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) (p : α → β → Bool) :\n  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} (t : Std.TreeMap.Raw α β cmp)\n  (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 α) (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) : 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) (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] (t : Std.ExtTreeSet α cmp)\n  (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", .declaration (Declaration.def {
+    name := `Std.DTreeMap.all
+    renderedStatement := "Std.DTreeMap.all.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} (t : Std.DTreeMap α β cmp)\n  (p : (a : α) → β a → Bool) : Bool"
+    isDeprecated := false
+  }
+)⟩,⟨"Std.DTreeMap.Raw", "Std.DTreeMap.Raw.all", .declaration (Declaration.def {
+    name := `Std.DTreeMap.Raw.all
+    renderedStatement := "Std.DTreeMap.Raw.all.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} (t : Std.DTreeMap.Raw α β cmp)\n  (p : (a : α) → β a → Bool) : Bool"
+    isDeprecated := false
+  }
+)⟩,⟨"Std.ExtDTreeMap", "Std.ExtDTreeMap.all", .declaration (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", .declaration (Declaration.def {
+    name := `Std.TreeMap.all
+    renderedStatement := "Std.TreeMap.all.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp) (p : α → β → Bool) :\n  Bool"
+    isDeprecated := false
+  }
+)⟩,⟨"Std.TreeMap.Raw", "Std.TreeMap.Raw.all", .declaration (Declaration.def {
+    name := `Std.TreeMap.Raw.all
+    renderedStatement := "Std.TreeMap.Raw.all.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : Std.TreeMap.Raw α β cmp)\n  (p : α → β → Bool) : Bool"
+    isDeprecated := false
+  }
+)⟩,⟨"Std.ExtTreeMap", "Std.ExtTreeMap.all", .declaration (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", .declaration (Declaration.def {
+    name := `Std.HashSet.all
+    renderedStatement := "Std.HashSet.all.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} (m : Std.HashSet α) (p : α → Bool) : Bool"
+    isDeprecated := false
+  }
+)⟩,⟨"Std.HashSet.Raw", "Std.HashSet.Raw.all", .declaration (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", .declaration (Declaration.def {
+    name := `Std.TreeSet.all
+    renderedStatement := "Std.TreeSet.all.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.TreeSet α cmp) (p : α → Bool) : Bool"
+    isDeprecated := false
+  }
+)⟩,⟨"Std.TreeSet.Raw", "Std.TreeSet.Raw.all", .declaration (Declaration.def {
+    name := `Std.TreeSet.Raw.all
+    renderedStatement := "Std.TreeSet.Raw.all.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.TreeSet.Raw α cmp) (p : α → Bool) : Bool"
+    isDeprecated := false
+  }
+)⟩,⟨"Std.ExtTreeSet", "Std.ExtTreeSet.all", .declaration (Declaration.def {
+    name := `Std.ExtTreeSet.all
+    renderedStatement := "Std.ExtTreeSet.all.{u} {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] (t : Std.ExtTreeSet α cmp)\n  (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", .declaration (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", .declaration (Declaration.def {
+    name := `Std.DHashMap.Raw.getD
+    renderedStatement := "Std.DHashMap.Raw.getD.{u, v} {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] (m : Std.DHashMap.Raw α β)\n  (a : α) (fallback : β a) : β a"
+    isDeprecated := false
+  }
+)⟩,⟨"Std.ExtDHashMap", "Std.ExtDHashMap.getD", .declaration (Declaration.def {
+    name := `Std.ExtDHashMap.getD
+    renderedStatement := "Std.ExtDHashMap.getD.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [LawfulBEq α]\n  (m : Std.ExtDHashMap α β) (a : α) (fallback : β a) : β a"
+    isDeprecated := false
+  }
+)⟩,⟨"Std.DTreeMap", "Std.DTreeMap.getD", .declaration (Declaration.def {
+    name := `Std.DTreeMap.getD
+    renderedStatement := "Std.DTreeMap.getD.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.LawfulEqCmp cmp]\n  (t : Std.DTreeMap α β cmp) (a : α) (fallback : β a) : β a"
+    isDeprecated := false
+  }
+)⟩,⟨"Std.DTreeMap.Raw", "Std.DTreeMap.Raw.getD", .declaration (Declaration.def {
+    name := `Std.DTreeMap.Raw.getD
+    renderedStatement := "Std.DTreeMap.Raw.getD.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.LawfulEqCmp cmp]\n  (t : Std.DTreeMap.Raw α β cmp) (a : α) (fallback : β a) : β a"
+    isDeprecated := false
+  }
+)⟩,⟨"Std.ExtDTreeMap", "Std.ExtDTreeMap.getD", .declaration (Declaration.def {
+    name := `Std.ExtDTreeMap.getD
+    renderedStatement := "Std.ExtDTreeMap.getD.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp]\n  [Std.LawfulEqCmp cmp] (t : Std.ExtDTreeMap α β cmp) (a : α) (fallback : β a) : β a"
+    isDeprecated := false
+  }
+)⟩,⟨"Std.HashMap", "Std.HashMap.getD", .declaration (Declaration.def {
+    name := `Std.HashMap.getD
+    renderedStatement := "Std.HashMap.getD.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} (m : Std.HashMap α β) (a : α)\n  (fallback : β) : β"
+    isDeprecated := false
+  }
+)⟩,⟨"Std.HashMap.Raw", "Std.HashMap.Raw.getD", .declaration (Declaration.def {
+    name := `Std.HashMap.Raw.getD
+    renderedStatement := "Std.HashMap.Raw.getD.{u, v} {α : Type u} {β : Type v} [BEq α] [Hashable α] (m : Std.HashMap.Raw α β) (a : α)\n  (fallback : β) : β"
+    isDeprecated := false
+  }
+)⟩,⟨"Std.ExtHashMap", "Std.ExtHashMap.getD", .declaration (Declaration.def {
+    name := `Std.ExtHashMap.getD
+    renderedStatement := "Std.ExtHashMap.getD.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α]\n  (m : Std.ExtHashMap α β) (a : α) (fallback : β) : β"
+    isDeprecated := false
+  }
+)⟩,⟨"Std.TreeMap", "Std.TreeMap.getD", .declaration (Declaration.def {
+    name := `Std.TreeMap.getD
+    renderedStatement := "Std.TreeMap.getD.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp) (a : α)\n  (fallback : β) : β"
+    isDeprecated := false
+  }
+)⟩,⟨"Std.TreeMap.Raw", "Std.TreeMap.Raw.getD", .declaration (Declaration.def {
+    name := `Std.TreeMap.Raw.getD
+    renderedStatement := "Std.TreeMap.Raw.getD.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : Std.TreeMap.Raw α β cmp) (a : α)\n  (fallback : β) : β"
+    isDeprecated := false
+  }
+)⟩,⟨"Std.ExtTreeMap", "Std.ExtTreeMap.getD", .declaration (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", .declaration (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", .declaration (Declaration.def {
+    name := `Std.HashSet.Raw.getD
+    renderedStatement := "Std.HashSet.Raw.getD.{u} {α : Type u} [BEq α] [Hashable α] (m : Std.HashSet.Raw α) (a fallback : α) : α"
+    isDeprecated := false
+  }
+)⟩,⟨"Std.ExtHashSet", "Std.ExtHashSet.getD", .declaration (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", .declaration (Declaration.def {
+    name := `Std.TreeSet.getD
+    renderedStatement := "Std.TreeSet.getD.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.TreeSet α cmp) (a fallback : α) : α"
+    isDeprecated := false
+  }
+)⟩,⟨"Std.TreeSet.Raw", "Std.TreeSet.Raw.getD", .declaration (Declaration.def {
+    name := `Std.TreeSet.Raw.getD
+    renderedStatement := "Std.TreeSet.Raw.getD.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.TreeSet.Raw α cmp) (a fallback : α) : α"
+    isDeprecated := false
+  }
+)⟩,⟨"Std.ExtTreeSet", "Std.ExtTreeSet.getD", .declaration (Declaration.def {
+    name := `Std.ExtTreeSet.getD
+    renderedStatement := "Std.ExtTreeSet.getD.{u} {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] (t : Std.ExtTreeSet α cmp)\n  (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", .declaration (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", .declaration (Declaration.def {
+    name := `Std.DHashMap.Raw.Const.get
+    renderedStatement := "Std.DHashMap.Raw.Const.get.{u, v} {α : Type u} {β : Type v} [BEq α] [Hashable α] (m : Std.DHashMap.Raw α fun x => β)\n  (a : α) (h : a ∈ m) : β"
+    isDeprecated := false
+  }
+)⟩,⟨"Std.ExtDHashMap", "Std.ExtDHashMap.get", .declaration (Declaration.def {
+    name := `Std.ExtDHashMap.get
+    renderedStatement := "Std.ExtDHashMap.get.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [LawfulBEq α]\n  (m : Std.ExtDHashMap α β) (a : α) (h : a ∈ m) : β a"
+    isDeprecated := false
+  }
+)⟩,⟨"Std.DTreeMap", "Std.DTreeMap.get", .declaration (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", .declaration (Declaration.def {
+    name := `Std.DTreeMap.Raw.get
+    renderedStatement := "Std.DTreeMap.Raw.get.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.LawfulEqCmp cmp]\n  (t : Std.DTreeMap.Raw α β cmp) (a : α) (h : a ∈ t) : β a"
+    isDeprecated := false
+  }
+)⟩,⟨"Std.ExtDTreeMap", "Std.ExtDTreeMap.get", .declaration (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", .declaration (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", .declaration (Declaration.def {
+    name := `Std.HashSet.Raw.get
+    renderedStatement := "Std.HashSet.Raw.get.{u} {α : Type u} [BEq α] [Hashable α] (m : Std.HashSet.Raw α) (a : α) (h : a ∈ m) : α"
+    isDeprecated := false
+  }
+)⟩,⟨"Std.ExtHashSet", "Std.ExtHashSet.get", .declaration (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", .declaration (Declaration.def {
+    name := `Std.TreeSet.get
+    renderedStatement := "Std.TreeSet.get.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.TreeSet α cmp) (a : α) (h : a ∈ t) : α"
+    isDeprecated := false
+  }
+)⟩,⟨"Std.TreeSet.Raw", "Std.TreeSet.Raw.get", .declaration (Declaration.def {
+    name := `Std.TreeSet.Raw.get
+    renderedStatement := "Std.TreeSet.Raw.get.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.TreeSet.Raw α cmp) (a : α) (h : a ∈ t) : α"
+    isDeprecated := false
+  }
+)⟩,⟨"Std.ExtTreeSet", "Std.ExtTreeSet.get", .declaration (Declaration.def {
+    name := `Std.ExtTreeSet.get
+    renderedStatement := "Std.ExtTreeSet.get.{u} {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] (t : Std.ExtTreeSet α cmp) (a : α)\n  (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

@@ -0,0 +1,31 @@
+/-
+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

@@ -0,0 +1,28 @@
+/-
+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

@@ -0,0 +1,19 @@
+/-
+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

@@ -0,0 +1,58 @@
+/-
+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 associativeQueryOperations : AssociationTable .subexpression
+    [`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] 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.declarationsInNamespace n .definitionsOnly)
+      |>.map Subexpression.declaration
+      |>.or (DataSource.getElem n)
+
+end AssociativeContainers
+
+def associativeContainers : Node :=
+  .section "associative-containers" "Associative containers" #[
+    .associationTable AssociativeContainers.associativeQueryOperations
+  ]
+
+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

@@ -0,0 +1,19 @@
+/-
+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

@@ -0,0 +1,19 @@
+/-
+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

@@ -0,0 +1,26 @@
+/-
+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

@@ -0,0 +1,19 @@
+/-
+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

@@ -0,0 +1,19 @@
+/-
+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

@@ -0,0 +1,19 @@
+/-
+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

@@ -0,0 +1,24 @@
+/-
+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

@@ -0,0 +1,19 @@
+/-
+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

@@ -0,0 +1,19 @@
+/-
+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

@@ -0,0 +1,30 @@
+/-
+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

@@ -0,0 +1,19 @@
+/-
+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

@@ -0,0 +1,19 @@
+/-
+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

@@ -0,0 +1,19 @@
+/-
+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

@@ -0,0 +1,19 @@
+/-
+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

@@ -0,0 +1,19 @@
+/-
+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

@@ -0,0 +1,18 @@
+/-
+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

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

doc/std/grove/grove-local.sh

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

doc/std/grove/lake-manifest.json

@@ -0,0 +1,25 @@
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/TwoFx/grove.git",
+   "type": "git",
+   "subDir": "backend",
+   "scope": "",
+   "rev": "e8127fc6554b99fb988ecdceb770a5e112afbe24",
+   "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

@@ -0,0 +1,18 @@
+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

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

doc/std/grove/update_invalidated.sh

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

script/mathlib-bench

@@ -5,8 +5,11 @@ 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/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-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_NUMBER=$(echo "$PR_RESPONSE" | jq '.number')
-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
+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

src/Init.lean

@@ -6,41 +6,41 @@ Authors: Leonardo de Moura
 module
 
 prelude
-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
+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

src/Init/BinderNameHint.lean

@@ -7,8 +7,10 @@ Authors: Joachim Breitner
 module
 
 prelude
-import Init.Prelude
-import Init.Tactics
+public import Init.Prelude
+public import Init.Tactics
+
+public section
 
 set_option linter.unusedVariables false in
 /--

src/Init/BinderPredicates.lean

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

src/Init/ByCases.lean

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

src/Init/Classical.lean

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

src/Init/Coe.lean

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

src/Init/Control.lean

@@ -6,13 +6,15 @@ Authors: Leonardo de Moura
 module
 
 prelude
-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
+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

src/Init/Control/Basic.lean

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

src/Init/Control/EState.lean

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

src/Init/Control/Except.lean

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

src/Init/Control/ExceptCps.lean

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

src/Init/Control/Id.lean

@@ -8,7 +8,9 @@ The identity Monad.
 module
 
 prelude
-import Init.Core
+public import Init.Core
+
+public section
 
 universe u
 
@@ -62,4 +64,7 @@ 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,7 +6,9 @@ Authors: Sebastian Ullrich, Leonardo de Moura, Mario Carneiro
 module
 
 prelude
-import Init.Control.Lawful.Basic
-import Init.Control.Lawful.Instances
-import Init.Control.Lawful.Lemmas
-import Init.Control.Lawful.MonadLift
+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

src/Init/Control/Lawful/Basic.lean

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

src/Init/Control/Lawful/Instances.lean

@@ -6,11 +6,13 @@ Authors: Sebastian Ullrich, Leonardo de Moura, Mario Carneiro
 module
 
 prelude
-import Init.Control.Lawful.Basic
-import all Init.Control.Except
-import all Init.Control.State
-import Init.Control.StateRef
-import Init.Ext
+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
 
 open Function
 

src/Init/Control/Lawful/Lemmas.lean

@@ -6,9 +6,11 @@ Authors: Kim Morrison
 module
 
 prelude
-import Init.Control.Lawful.Basic
-import Init.RCases
-import Init.ByCases
+public import Init.Control.Lawful.Basic
+public import Init.RCases
+public import Init.ByCases
+
+public section
 
 -- 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,6 +6,8 @@ Authors: Paul Reichert
 module
 
 prelude
-import Init.Control.Lawful.MonadLift.Basic
-import Init.Control.Lawful.MonadLift.Lemmas
-import Init.Control.Lawful.MonadLift.Instances
+public import Init.Control.Lawful.MonadLift.Basic
+public import Init.Control.Lawful.MonadLift.Lemmas
+public import Init.Control.Lawful.MonadLift.Instances
+
+public section

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

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

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

@@ -6,13 +6,16 @@ Authors: Quang Dao, Paul Reichert
 module
 
 prelude
-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
+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
 
 universe u v w x
 
@@ -135,3 +138,11 @@ 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,8 +6,10 @@ Authors: Quang Dao
 module
 
 prelude
-import Init.Control.Lawful.Basic
-import Init.Control.Lawful.MonadLift.Basic
+public import Init.Control.Lawful.Basic
+public import Init.Control.Lawful.MonadLift.Basic
+
+public section
 
 universe u v w
 

src/Init/Control/Option.lean

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

src/Init/Control/Reader.lean

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

src/Init/Control/State.lean

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

src/Init/Control/StateCps.lean

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

src/Init/Control/StateRef.lean

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

src/Init/Conv.lean

@@ -8,8 +8,10 @@ Notation for operators defined at Prelude.lean
 module
 
 prelude
-import Init.Tactics
-meta import Init.Meta
+public import Init.Tactics
+public meta import Init.Meta
+
+public section
 
 namespace Lean.Parser.Tactic.Conv
 
@@ -339,6 +341,12 @@ 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 th etarget 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,8 +8,10 @@ notation, basic datatypes and type classes
 module
 
 prelude
-meta import Init.Prelude
-import Init.SizeOf
+public meta import Init.Prelude
+public import Init.SizeOf
+
+public section
 set_option linter.missingDocs true -- keep it documented
 
 @[expose] section

src/Init/Data.lean

@@ -6,44 +6,48 @@ Authors: Leonardo de Moura
 module
 
 prelude
-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
+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 section

src/Init/Data/AC.lean

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

src/Init/Data/Array.lean

@@ -6,27 +6,29 @@ Authors: Gabriel Ebner
 module
 
 prelude
-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
+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

src/Init/Data/Array/Attach.lean

@@ -6,10 +6,12 @@ Authors: Joachim Breitner, Mario Carneiro
 module
 
 prelude
-import Init.Data.Array.Mem
-import Init.Data.Array.Lemmas
-import Init.Data.Array.Count
-import all Init.Data.List.Attach
+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
 
 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,15 +6,17 @@ Authors: Leonardo de Moura
 module
 
 prelude
-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
+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
 
 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/BasicAux.lean

@@ -6,9 +6,11 @@ Authors: Leonardo de Moura
 module
 
 prelude
-import all Init.Data.Array.Basic
-import Init.Data.Nat.Linear
-import Init.NotationExtra
+public import all Init.Data.Array.Basic
+public import Init.Data.Nat.Linear
+public import Init.NotationExtra
+
+public section
 
 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,9 +6,11 @@ Authors: Leonardo de Moura
 module
 
 prelude
-import Init.Data.Array.Basic
-import Init.Data.Int.DivMod.Lemmas
-import Init.Omega
+public import Init.Data.Array.Basic
+public import Init.Data.Int.DivMod.Lemmas
+public import Init.Omega
+
+public section
 universe u v
 
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.

src/Init/Data/Array/Bootstrap.lean

@@ -7,8 +7,10 @@ Authors: Mario Carneiro
 module
 
 prelude
-import Init.Data.List.TakeDrop
-import all Init.Data.Array.Basic
+public import Init.Data.List.TakeDrop
+public import all Init.Data.Array.Basic
+
+public section
 
 /-!
 ## Bootstrapping theorems about arrays

src/Init/Data/Array/Count.lean

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

src/Init/Data/Array/DecidableEq.lean

@@ -6,10 +6,12 @@ Authors: Leonardo de Moura
 module
 
 prelude
-import all Init.Data.Array.Basic
-import Init.Data.BEq
-import Init.Data.List.Nat.BEq
-import Init.ByCases
+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
 
 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,10 +6,12 @@ Authors: Kim Morrison
 module
 
 prelude
-import all Init.Data.Array.Basic
-import Init.Data.Array.Lemmas
-import Init.Data.List.Nat.Erase
-import Init.Data.List.Nat.Basic
+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
 
 /-!
 # Lemmas about `Array.eraseP`, `Array.erase`, and `Array.eraseIdx`.

src/Init/Data/Array/Extract.lean

@@ -6,8 +6,10 @@ Authors: Kim Morrison
 module
 
 prelude
-import Init.Data.Array.Lemmas
-import Init.Data.List.Nat.TakeDrop
+public import Init.Data.Array.Lemmas
+public import Init.Data.List.Nat.TakeDrop
+
+public section
 
 /-!
 # Lemmas about `Array.extract`
@@ -46,15 +48,45 @@ theorem size_extract_of_le {as : Array α} {i j : Nat} (h : j ≤ as.size) :
   simp
   omega
 
-@[simp, grind =]
-theorem extract_push {as : Array α} {b : α} {start stop : Nat} (h : stop ≤ as.size) :
+@[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) :
     (as.push b).extract start stop = as.extract start stop := by
-  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)]
+  rw [extract_push, if_pos h]
 
 @[simp, grind =]
 theorem extract_eq_pop {as : Array α} {stop : Nat} (h : stop = as.size - 1) :

src/Init/Data/Array/FinRange.lean

@@ -6,8 +6,10 @@ Authors: François G. Dorais
 module
 
 prelude
-import Init.Data.List.FinRange
-import Init.Data.Array.OfFn
+public import Init.Data.List.FinRange
+public import Init.Data.Array.OfFn
+
+public section
 
 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,11 +6,13 @@ Authors: Kim Morrison
 module
 
 prelude
-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
+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
 
 /-!
 # Lemmas about `Array.findSome?`, `Array.find?, `Array.findIdx`, `Array.findIdx?`, `Array.idxOf`.

src/Init/Data/Array/GetLit.lean

@@ -7,7 +7,9 @@ Authors: Leonardo de Moura
 module
 
 prelude
-import Init.Data.Array.Basic
+public import Init.Data.Array.Basic
+
+public section
 
 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,8 +6,10 @@ Authors: Kim Morrison
 module
 
 prelude
-import Init.Data.Array.Lemmas
-import Init.Data.List.Nat.InsertIdx
+public import Init.Data.Array.Lemmas
+public import Init.Data.List.Nat.InsertIdx
+
+public section
 
 /-!
 # insertIdx

src/Init/Data/Array/InsertionSort.lean

@@ -6,7 +6,9 @@ Authors: Leonardo de Moura
 module
 
 prelude
-import Init.Data.Array.Basic
+public import Init.Data.Array.Basic
+
+public section
 
 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,21 +6,23 @@ Authors: Mario Carneiro, Kim Morrison
 module
 
 prelude
-import Init.Data.Nat.Lemmas
-import Init.Data.List.Range
-import all Init.Data.List.Control
-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
-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
+public import Init.Data.Nat.Lemmas
+public import Init.Data.List.Range
+public import all Init.Data.List.Control
+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 all Init.Data.Array.Bootstrap
+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
+
+public section
 
 /-!
 ## Theorems about `Array`.

src/Init/Data/Array/Lex.lean

@@ -6,5 +6,7 @@ Author: Kim Morrison
 module
 
 prelude
-import Init.Data.Array.Lex.Basic
-import Init.Data.Array.Lex.Lemmas
+public import Init.Data.Array.Lex.Basic
+public import Init.Data.Array.Lex.Lemmas
+
+public section

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

@@ -6,9 +6,11 @@ Author: Kim Morrison
 module
 
 prelude
-import Init.Data.Array.Basic
-import Init.Data.Nat.Lemmas
-import Init.Data.Range
+public import Init.Data.Array.Basic
+public import Init.Data.Nat.Lemmas
+public import Init.Data.Range
+
+public section
 
 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/Lex/Lemmas.lean

@@ -6,9 +6,11 @@ Author: Kim Morrison
 module
 
 prelude
-import all Init.Data.Array.Lex.Basic
-import Init.Data.Array.Lemmas
-import Init.Data.List.Lex
+public import all Init.Data.Array.Lex.Basic
+public import Init.Data.Array.Lemmas
+public import Init.Data.List.Lex
+
+public section
 
 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/MapIdx.lean

@@ -6,11 +6,13 @@ Authors: Mario Carneiro, Kim Morrison
 module
 
 prelude
-import all Init.Data.Array.Basic
-import Init.Data.Array.Lemmas
-import Init.Data.Array.Attach
-import Init.Data.Array.OfFn
-import all Init.Data.List.MapIdx
+public import all Init.Data.Array.Basic
+public import Init.Data.Array.Lemmas
+public import Init.Data.Array.Attach
+public import Init.Data.Array.OfFn
+public import all Init.Data.List.MapIdx
+
+public section
 
 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/Mem.lean

@@ -6,9 +6,11 @@ Authors: Leonardo de Moura, Joachim Breitner
 module
 
 prelude
-import Init.Data.Array.Basic
-import Init.Data.Nat.Linear
-import Init.Data.List.BasicAux
+public import Init.Data.Array.Basic
+public import Init.Data.Nat.Linear
+public import Init.Data.List.BasicAux
+
+public section
 
 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/Monadic.lean

@@ -6,11 +6,13 @@ Authors: Kim Morrison
 module
 
 prelude
-import all Init.Data.List.Control
-import all Init.Data.Array.Basic
-import Init.Data.Array.Lemmas
-import Init.Data.Array.Attach
-import Init.Data.List.Monadic
+public import all Init.Data.List.Control
+public import all Init.Data.Array.Basic
+public import Init.Data.Array.Lemmas
+public import Init.Data.Array.Attach
+public import Init.Data.List.Monadic
+
+public section
 
 /-!
 # Lemmas about `Array.forIn'` and `Array.forIn`.

src/Init/Data/Array/OfFn.lean

@@ -6,11 +6,13 @@ Authors: Kim Morrison
 module
 
 prelude
-import all Init.Data.Array.Basic
-import Init.Data.Array.Lemmas
-import Init.Data.Array.Monadic
-import Init.Data.List.OfFn
-import Init.Data.List.FinRange
+public import all Init.Data.Array.Basic
+public import Init.Data.Array.Lemmas
+public import Init.Data.Array.Monadic
+public import Init.Data.List.OfFn
+public import Init.Data.List.FinRange
+
+public section
 
 /-!
 # Theorems about `Array.ofFn`

src/Init/Data/Array/Perm.lean

@@ -6,9 +6,11 @@ Authors: Kim Morrison
 module
 
 prelude
-import Init.Data.List.Nat.Perm
-import all Init.Data.Array.Basic
-import Init.Data.Array.Lemmas
+public import Init.Data.List.Nat.Perm
+public import all Init.Data.Array.Basic
+public import Init.Data.Array.Lemmas
+
+public section
 
 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/QSort.lean

@@ -6,4 +6,6 @@ Authors: Kim Morrison
 module
 
 prelude
-import Init.Data.Array.QSort.Basic
+public import Init.Data.Array.QSort.Basic
+
+public section

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

@@ -6,8 +6,10 @@ Authors: Leonardo de Moura
 module
 
 prelude
-import Init.Data.Vector.Basic
-import Init.Data.Ord
+public import Init.Data.Vector.Basic
+public import Init.Data.Ord
+
+public section
 
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 -- We do not enable `linter.indexVariables` because it is helpful to name index variables `lo`, `mid`, `hi`, etc.
@@ -55,7 +57,7 @@ def qpartition {n} (as : Vector α n) (lt : α → α → Bool) (lo hi : Nat) (w
 /--
 In-place quicksort.
 
-`qsort as lt lo hi` sorts the subarray `as[lo:hi+1]` in-place using `lt` to compare elements.
+`qsort as lt lo hi` sorts the subarray `as[lo...=hi]` in-place using `lt` to compare elements.
 -/
 @[inline] def qsort (as : Array α) (lt : α → α → Bool := by exact (· < ·))
     (lo := 0) (hi := as.size - 1) : Array α :=
@@ -65,7 +67,7 @@ In-place quicksort.
       let ⟨⟨mid, hmid⟩, as⟩ := qpartition as lt lo hi
       if h₂ : mid ≥ hi then
         -- This only occurs when `hi ≤ lo`,
-        -- and thus `as[lo:hi+1]` is trivially already sorted.
+        -- and thus `as[lo...(hi+1)]` is trivially already sorted.
         as
       else
         -- Otherwise, we recursively sort the two subarrays.

src/Init/Data/Array/Range.lean

@@ -6,12 +6,14 @@ Authors: Kim Morrison
 module
 
 prelude
-import Init.Data.Array.Lemmas
-import all Init.Data.Array.Basic
-import all Init.Data.Array.OfFn
-import Init.Data.Array.MapIdx
-import Init.Data.Array.Zip
-import Init.Data.List.Nat.Range
+public import Init.Data.Array.Lemmas
+public import all Init.Data.Array.Basic
+public import all Init.Data.Array.OfFn
+public import Init.Data.Array.MapIdx
+public import Init.Data.Array.Zip
+public import Init.Data.List.Nat.Range
+
+public section
 
 /-!
 # Lemmas about `Array.range'`, `Array.range`, and `Array.zipIdx`

src/Init/Data/Array/Set.lean

@@ -6,7 +6,9 @@ Authors: Leonardo de Moura, Mario Carneiro
 module
 
 prelude
-import Init.Tactics
+public import Init.Tactics
+
+public section
 
 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/Subarray.lean

@@ -6,7 +6,10 @@ Authors: Leonardo de Moura
 module
 
 prelude
-import Init.Data.Array.Basic
+public import Init.Data.Array.Basic
+public import Init.Data.Slice.Basic
+
+public section
 
 set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 set_option linter.missingDocs true
@@ -14,14 +17,9 @@ set_option linter.missingDocs true
 universe u v w
 
 /--
-A region of some underlying array.
-
-A subarray contains an array together with the start and end indices of a region of interest.
-Subarrays can be used to avoid copying or allocating space, while being more convenient than
-tracking the bounds by hand. The region of interest consists of every index that is both greater
-than or equal to `start` and strictly less than `stop`.
+Internal representation of `Subarray`, which is an abbreviation for `Slice SubarrayData`.
 -/
-structure Subarray (α : Type u) where
+structure Std.Slice.Internal.SubarrayData (α : Type u) where
   /-- The underlying array. -/
   array : Array α
   /-- The starting index of the region of interest (inclusive). -/
@@ -42,6 +40,40 @@ structure Subarray (α : Type u) where
   -/
   stop_le_array_size : stop ≤ array.size
 
+open Std.Slice
+
+/--
+A region of some underlying array.
+
+A subarray contains an array together with the start and end indices of a region of interest.
+Subarrays can be used to avoid copying or allocating space, while being more convenient than
+tracking the bounds by hand. The region of interest consists of every index that is both greater
+than or equal to `start` and strictly less than `stop`.
+-/
+abbrev Subarray (α : Type u) := Std.Slice (Internal.SubarrayData α)
+
+instance {α : Type u} : Self (Std.Slice (Internal.SubarrayData α)) (Subarray α) where
+
+@[always_inline, inline, expose, inherit_doc Internal.SubarrayData.array]
+def Subarray.array (xs : Subarray α) : Array α :=
+  xs.internalRepresentation.array
+
+@[always_inline, inline, expose, inherit_doc Internal.SubarrayData.start]
+def Subarray.start (xs : Subarray α) : Nat :=
+  xs.internalRepresentation.start
+
+@[always_inline, inline, expose, inherit_doc Internal.SubarrayData.stop]
+def Subarray.stop (xs : Subarray α) : Nat :=
+  xs.internalRepresentation.stop
+
+@[always_inline, inline, expose, inherit_doc Internal.SubarrayData.start_le_stop]
+def Subarray.start_le_stop (xs : Subarray α) : xs.start ≤ xs.stop :=
+  xs.internalRepresentation.start_le_stop
+
+@[always_inline, inline, expose, inherit_doc Internal.SubarrayData.stop_le_array_size]
+def Subarray.stop_le_array_size (xs : Subarray α) : xs.stop ≤ xs.array.size :=
+  xs.internalRepresentation.stop_le_array_size
+
 namespace Subarray
 
 /--
@@ -51,8 +83,8 @@ def size (s : Subarray α) : Nat :=
   s.stop - s.start
 
 theorem size_le_array_size {s : Subarray α} : s.size ≤ s.array.size := by
-  let {array, start, stop, start_le_stop, stop_le_array_size} := s
-  simp [size]
+  let ⟨{array, start, stop, start_le_stop, stop_le_array_size}⟩ := s
+  simp only [size, ge_iff_le]
   apply Nat.le_trans (Nat.sub_le stop start)
   assumption
 
@@ -65,7 +97,7 @@ def get (s : Subarray α) (i : Fin s.size) : α :=
   have : s.start + i.val < s.array.size := by
    apply Nat.lt_of_lt_of_le _ s.stop_le_array_size
    have := i.isLt
-   simp [size] at this
+   simp only [size] at this
    rw [Nat.add_comm]
    exact Nat.add_lt_of_lt_sub this
   s.array[s.start + i.val]
@@ -102,7 +134,9 @@ Examples:
 -/
 def popFront (s : Subarray α) : Subarray α :=
   if h : s.start < s.stop then
-    { s with start := s.start + 1, start_le_stop := Nat.le_of_lt_succ (Nat.add_lt_add_right h 1) }
+    ⟨{ s.internalRepresentation with
+        start := s.start + 1,
+        start_le_stop := Nat.le_of_lt_succ (Nat.add_lt_add_right h 1) }⟩
   else
     s
 
@@ -111,12 +145,13 @@ The empty subarray.
 
 This empty subarray is backed by an empty array.
 -/
-protected def empty : Subarray α where
-  array := #[]
-  start := 0
-  stop := 0
-  start_le_stop := Nat.le_refl 0
-  stop_le_array_size := Nat.le_refl 0
+protected def empty : Subarray α := ⟨{
+    array := #[]
+    start := 0
+    stop := 0
+    start_le_stop := Nat.le_refl 0
+    stop_le_array_size := Nat.le_refl 0
+  }⟩
 
 instance : EmptyCollection (Subarray α) :=
   ⟨Subarray.empty⟩
@@ -410,24 +445,24 @@ Additionally, the starting index is clamped to the ending index.
 def toSubarray (as : Array α) (start : Nat := 0) (stop : Nat := as.size) : Subarray α :=
   if h₂ : stop ≤ as.size then
     if h₁ : start ≤ stop then
-      { array := as, start := start, stop := stop,
-        start_le_stop := h₁, stop_le_array_size := h₂ }
+      ⟨{ array := as, start := start, stop := stop,
+         start_le_stop := h₁, stop_le_array_size := h₂ }⟩
     else
-      { array := as, start := stop, stop := stop,
-        start_le_stop := Nat.le_refl _, stop_le_array_size := h₂ }
+      ⟨{ array := as, start := stop, stop := stop,
+         start_le_stop := Nat.le_refl _, stop_le_array_size := h₂ }⟩
   else
     if h₁ : start ≤ as.size then
-      { array := as,
-        start := start,
-        stop := as.size,
-        start_le_stop := h₁,
-        stop_le_array_size := Nat.le_refl _ }
+      ⟨{ array := as,
+         start := start,
+         stop := as.size,
+         start_le_stop := h₁,
+         stop_le_array_size := Nat.le_refl _ }⟩
     else
-      { array := as,
-        start := as.size,
-        stop := as.size,
-        start_le_stop := Nat.le_refl _,
-        stop_le_array_size := Nat.le_refl _ }
+      ⟨{ array := as,
+         start := as.size,
+         stop := as.size,
+         start_le_stop := Nat.le_refl _,
+         stop_le_array_size := Nat.le_refl _ }⟩
 
 /--
 Allocates a new array that contains the contents of the subarray.

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

@@ -7,9 +7,11 @@ Authors: David Thrane Christiansen
 module
 
 prelude
-import Init.Data.Array.Basic
-import all Init.Data.Array.Subarray
-import Init.Omega
+public import Init.Data.Array.Basic
+public import all Init.Data.Array.Subarray
+public import Init.Omega
+
+public section
 
 /-
 This module contains splitting operations on subarrays that crucially rely on `omega` for proof
@@ -21,44 +23,24 @@ set_option linter.listVariables true -- Enforce naming conventions for `List`/`A
 set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace Subarray
-/--
-Splits a subarray into two parts, the first of which contains the first `i` elements and the second
-of which contains the remainder.
--/
-def split (s : Subarray α) (i : Fin s.size.succ) : (Subarray α × Subarray α) :=
-  let ⟨i', isLt⟩ := i
-  have := s.start_le_stop
-  have := s.stop_le_array_size
-  have : s.start + i' ≤ s.stop := by
-    simp only [size] at isLt
-    omega
-  let pre := {s with
-    stop := s.start + i',
-    start_le_stop := by omega,
-    stop_le_array_size := by omega
-  }
-  let post := {s with
-    start := s.start + i'
-    start_le_stop := by assumption
-  }
-  (pre, post)
 
 /--
 Removes the first `i` elements of the subarray. If there are `i` or fewer elements, the resulting
 subarray is empty.
 -/
-def drop (arr : Subarray α) (i : Nat) : Subarray α where
+def drop (arr : Subarray α) (i : Nat) : Subarray α := ⟨{
   array := arr.array
   start := min (arr.start + i) arr.stop
   stop := arr.stop
   start_le_stop := by omega
   stop_le_array_size := arr.stop_le_array_size
+}⟩
 
 /--
 Keeps only the first `i` elements of the subarray. If there are `i` or fewer elements, the resulting
 subarray is empty.
 -/
-def take (arr : Subarray α) (i : Nat) : Subarray α where
+def take (arr : Subarray α) (i : Nat) : Subarray α := ⟨{
   array := arr.array
   start := arr.start
   stop := min (arr.start + i) arr.stop
@@ -68,3 +50,11 @@ def take (arr : Subarray α) (i : Nat) : Subarray α where
   stop_le_array_size := by
     have := arr.stop_le_array_size
     omega
+}⟩
+
+/--
+Splits a subarray into two parts, the first of which contains the first `i` elements and the second
+of which contains the remainder.
+-/
+def split (s : Subarray α) (i : Fin s.size.succ) : (Subarray α × Subarray α) :=
+  (s.take i, s.drop i)

src/Init/Data/Array/TakeDrop.lean

@@ -6,9 +6,11 @@ Authors: Markus Himmel
 module
 
 prelude
-import all Init.Data.Array.Basic
-import Init.Data.Array.Lemmas
-import Init.Data.List.Nat.TakeDrop
+public import all Init.Data.Array.Basic
+public import Init.Data.Array.Lemmas
+public import Init.Data.List.Nat.TakeDrop
+
+public section
 
 /-!
 These lemmas are used in the internals of HashMap.

src/Init/Data/Array/Zip.lean

@@ -6,9 +6,11 @@ Authors: Kim Morrison
 module
 
 prelude
-import all Init.Data.Array.Basic
-import Init.Data.Array.TakeDrop
-import Init.Data.List.Zip
+public import all Init.Data.Array.Basic
+public import Init.Data.Array.TakeDrop
+public import Init.Data.List.Zip
+
+public section
 
 /-!
 # Lemmas about `Array.zip`, `Array.zipWith`, `Array.zipWithAll`, and `Array.unzip`.

src/Init/Data/BEq.lean

@@ -6,7 +6,9 @@ Authors: Mario Carneiro, Markus Himmel
 module
 
 prelude
-import Init.Data.Bool
+public import Init.Data.Bool
+
+public section
 
 set_option linter.missingDocs true