doc-string

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

.github/workflows/awaiting-manual.yml

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

.github/workflows/build-template.yml

@@ -107,7 +107,6 @@ 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 }}
@@ -249,7 +248,6 @@ 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,7 +145,6 @@ jobs:
             // use large runners where available (original repo)
             let large = ${{ github.repository == 'leanprover/lean4' }};
             const isPr = "${{ github.event_name }}" == "pull_request";
-            const isPushToMaster = "${{ github.event_name }}" == "push" && "${{ github.ref_name }}" == "master";
             let matrix = [
               /* TODO: to be updated to new LLVM
               {
@@ -168,13 +167,11 @@ 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 developers get PR toolchains (so secondary is sufficient)
+                // 1. To run it in PRs so developrs get PR toolchains (so secondary is sufficient)
                 // 2. To skip it in merge queues as it takes longer than the
                 //    Linux lake build and adds little value in the merge queue
                 // 3. To run it in release (obviously)
-                // 4. To run it for pushes to master so that pushes to master have a Linux toolchain
-                //    available as an artifact for Grove to use.
-                "check-level": (isPr || isPushToMaster) ? 0 : 2,
+                "check-level": isPr ? 0 : 2,
                 "secondary": isPr,
                 "shell": "nix develop .#oldGlibc -c bash -euxo pipefail {0}",
                 "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-linux-gnu.tar.zst",
@@ -424,6 +421,6 @@ jobs:
           GITHUB_TOKEN: ${{ secrets.RELEASE_INDEX_TOKEN }}
       - name: Update toolchain on mathlib4's nightly-testing branch
         run: |
-          gh workflow -R leanprover-community/mathlib4-nightly-testing run nightly_bump_toolchain.yml
+          gh workflow -R leanprover-community/mathlib4 run nightly_bump_toolchain.yml
         env:
           GITHUB_TOKEN: ${{ secrets.MATHLIB4_BOT }}

.github/workflows/grove.yml

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

doc/dev/ffi.md

@@ -131,21 +131,14 @@ Thus `[init]` functions are run iff their module is imported, regardless of whet
 
 The initializer for module `A.B` is called `initialize_A_B` and will automatically initialize any imported modules.
 Module initializers are idempotent (when run with the same `builtin` flag), but not thread-safe.
-
-**Important for process-related functionality**: If your application needs to use process-related functions from libuv, such as `Std.Internal.IO.Process.getProcessTitle` and `Std.Internal.IO.Process.setProcessTitle`, you must call `lean_setup_args(argc, argv)` (which returns a potentially modified `argv` that must be used in place of the original) **before** calling `lean_initialize()` or `lean_initialize_runtime_module()`. This sets up process handling capabilities correctly, which is essential for certain system-level operations that Lean's runtime may depend on.
-
 Together with initialization of the Lean runtime, you should execute code like the following exactly once before accessing any Lean declarations:
-
 ```c
 void lean_initialize_runtime_module();
 void lean_initialize();
-char ** lean_setup_args(int argc, char ** argv);
-
 lean_object * initialize_A_B(uint8_t builtin, lean_object *);
 lean_object * initialize_C(uint8_t builtin, lean_object *);
 ...
 
-argv = lean_setup_args(argc, argv); // if using process-related functionality
 lean_initialize_runtime_module();
 //lean_initialize();  // necessary (and replaces `lean_initialize_runtime_module`) if you (indirectly) access the `Lean` package
 

doc/dev/index.md

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

doc/std/grove/.gitignore

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

doc/std/grove/GroveStdlib/Generated.lean

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

@@ -1,486 +0,0 @@
-import Grove.Framework
-
-/-
-This file is autogenerated by grove. You can manually edit it, for example to resolve merge
-conflicts, but be careful.
--/
-
-open Grove.Framework Widget
-
-namespace GroveStdlib.Generated.«associative-query-operations»
-
-def «01f88623-fa5f-4380-9772-b30f2fec5c94» : AssociationTable.Fact .subexpression where
-  widgetId := "associative-query-operations"
-  factId := "01f88623-fa5f-4380-9772-b30f2fec5c94"
-  rowId := "01f88623-fa5f-4380-9772-b30f2fec5c94"
-  rowState := #[⟨"Std.DHashMap", "Std.DHashMap.isEmpty", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.DHashMap.isEmpty,
-      renderedStatement := "Std.DHashMap.isEmpty.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} (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

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

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

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

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

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

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

@@ -1,58 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel
--/
-import Grove.Framework
-
-open Grove.Framework Widget
-
-namespace GroveStdlib.Std.CoreTypesAndOperations
-
-namespace Containers
-
-namespace SequentialContainers
-
-end SequentialContainers
-
-def sequentialContainers : Node :=
-  .section "sequential-containers" "Sequential containers" #[]
-
-namespace AssociativeContainers
-
-def 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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

doc/std/grove/Main.lean

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

doc/std/grove/README.md

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

doc/std/grove/grove-local.sh

@@ -1,10 +0,0 @@
-#!/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

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

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

doc/std/grove/lean-toolchain

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

doc/std/grove/update_invalidated.sh

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

script/mathlib-bench

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

src/Init/BinderNameHint.lean

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

src/Init/BinderPredicates.lean

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

src/Init/ByCases.lean

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

src/Init/Classical.lean

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

src/Init/Coe.lean

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

src/Init/Control.lean

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

src/Init/Control/Basic.lean

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

src/Init/Control/EState.lean

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

src/Init/Control/Except.lean

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

src/Init/Control/ExceptCps.lean

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

src/Init/Control/Id.lean

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

src/Init/Control/Lawful.lean

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

src/Init/Control/Lawful/Basic.lean

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

src/Init/Control/Lawful/Instances.lean

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

src/Init/Control/Lawful/Lemmas.lean

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

src/Init/Control/Lawful/MonadLift.lean

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

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

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

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

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

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

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

src/Init/Control/Option.lean

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

src/Init/Control/Reader.lean

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

src/Init/Control/State.lean

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

src/Init/Control/StateCps.lean

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

src/Init/Control/StateRef.lean

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

src/Init/Conv.lean

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

src/Init/Data.lean

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

src/Init/Data/AC.lean

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

src/Init/Data/Array.lean

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

src/Init/Data/Array/Attach.lean

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

src/Init/Data/Array/Basic.lean

@@ -6,17 +6,15 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Init.WFTactics
-public import Init.Data.Nat.Basic
-public import Init.Data.Fin.Basic
-public import Init.Data.UInt.BasicAux
-public import Init.Data.Repr
-public import Init.Data.ToString.Basic
-public import Init.GetElem
-public import all Init.Data.List.ToArrayImpl
-public import all Init.Data.Array.Set
-
-public section
+import Init.WFTactics
+import Init.Data.Nat.Basic
+import Init.Data.Fin.Basic
+import Init.Data.UInt.BasicAux
+import Init.Data.Repr
+import Init.Data.ToString.Basic
+import Init.GetElem
+import all Init.Data.List.ToArrayImpl
+import all Init.Data.Array.Set
 
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 set_option linter.indexVariables true -- Enforce naming conventions for index variables.

src/Init/Data/Array/BasicAux.lean

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

src/Init/Data/Array/BinSearch.lean

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

src/Init/Data/Array/Bootstrap.lean

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

src/Init/Data/Array/Count.lean

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

src/Init/Data/Array/DecidableEq.lean

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

src/Init/Data/Array/Erase.lean

@@ -6,12 +6,10 @@ Authors: Kim Morrison
 module
 
 prelude
-public import all Init.Data.Array.Basic
-public import Init.Data.Array.Lemmas
-public import Init.Data.List.Nat.Erase
-public import Init.Data.List.Nat.Basic
-
-public section
+import all Init.Data.Array.Basic
+import Init.Data.Array.Lemmas
+import Init.Data.List.Nat.Erase
+import Init.Data.List.Nat.Basic
 
 /-!
 # Lemmas about `Array.eraseP`, `Array.erase`, and `Array.eraseIdx`.

src/Init/Data/Array/Extract.lean

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

src/Init/Data/Array/FinRange.lean

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

src/Init/Data/Array/Find.lean

@@ -6,13 +6,11 @@ Authors: Kim Morrison
 module
 
 prelude
-public import Init.Data.List.Nat.Find
-public import all Init.Data.Array.Basic
-public import Init.Data.Array.Lemmas
-public import Init.Data.Array.Attach
-public import Init.Data.Array.Range
-
-public section
+import Init.Data.List.Nat.Find
+import all Init.Data.Array.Basic
+import Init.Data.Array.Lemmas
+import Init.Data.Array.Attach
+import Init.Data.Array.Range
 
 /-!
 # Lemmas about `Array.findSome?`, `Array.find?, `Array.findIdx`, `Array.findIdx?`, `Array.idxOf`.

src/Init/Data/Array/GetLit.lean

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

src/Init/Data/Array/InsertIdx.lean

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

src/Init/Data/Array/InsertionSort.lean

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

src/Init/Data/Array/Lemmas.lean

@@ -6,23 +6,21 @@ Authors: Mario Carneiro, Kim Morrison
 module
 
 prelude
-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
+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
 
 /-!
 ## Theorems about `Array`.

src/Init/Data/Array/Lex.lean

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

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

@@ -6,11 +6,9 @@ Author: Kim Morrison
 module
 
 prelude
-public import Init.Data.Array.Basic
-public import Init.Data.Nat.Lemmas
-public import Init.Data.Range
-
-public section
+import Init.Data.Array.Basic
+import Init.Data.Nat.Lemmas
+import Init.Data.Range
 
 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,11 +6,9 @@ Author: Kim Morrison
 module
 
 prelude
-public import all Init.Data.Array.Lex.Basic
-public import Init.Data.Array.Lemmas
-public import Init.Data.List.Lex
-
-public section
+import all Init.Data.Array.Lex.Basic
+import Init.Data.Array.Lemmas
+import Init.Data.List.Lex
 
 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,13 +6,11 @@ Authors: Mario Carneiro, Kim Morrison
 module
 
 prelude
-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
+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
 
 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,11 +6,9 @@ Authors: Leonardo de Moura, Joachim Breitner
 module
 
 prelude
-public import Init.Data.Array.Basic
-public import Init.Data.Nat.Linear
-public import Init.Data.List.BasicAux
-
-public section
+import Init.Data.Array.Basic
+import Init.Data.Nat.Linear
+import Init.Data.List.BasicAux
 
 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,13 +6,11 @@ Authors: Kim Morrison
 module
 
 prelude
-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
+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
 
 /-!
 # Lemmas about `Array.forIn'` and `Array.forIn`.

src/Init/Data/Array/OfFn.lean

@@ -6,13 +6,11 @@ Authors: Kim Morrison
 module
 
 prelude
-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
+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
 
 /-!
 # Theorems about `Array.ofFn`

src/Init/Data/Array/Perm.lean

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

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

@@ -6,10 +6,8 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Init.Data.Vector.Basic
-public import Init.Data.Ord
-
-public section
+import Init.Data.Vector.Basic
+import Init.Data.Ord
 
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 -- We do not enable `linter.indexVariables` because it is helpful to name index variables `lo`, `mid`, `hi`, etc.
@@ -57,7 +55,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]` in-place using `lt` to compare elements.
+`qsort as lt lo hi` sorts the subarray `as[lo:hi+1]` in-place using `lt` to compare elements.
 -/
 @[inline] def qsort (as : Array α) (lt : α → α → Bool := by exact (· < ·))
     (lo := 0) (hi := as.size - 1) : Array α :=
@@ -67,7 +65,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,14 +6,12 @@ Authors: Kim Morrison
 module
 
 prelude
-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
+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
 
 /-!
 # Lemmas about `Array.range'`, `Array.range`, and `Array.zipIdx`

src/Init/Data/Array/Set.lean

@@ -6,9 +6,7 @@ Authors: Leonardo de Moura, Mario Carneiro
 module
 
 prelude
-public import Init.Tactics
-
-public section
+import Init.Tactics
 
 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,10 +6,7 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Init.Data.Array.Basic
-public import Init.Data.Slice.Basic
-
-public section
+import Init.Data.Array.Basic
 
 set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 set_option linter.missingDocs true
@@ -17,9 +14,14 @@ set_option linter.missingDocs true
 universe u v w
 
 /--
-Internal representation of `Subarray`, which is an abbreviation for `Slice SubarrayData`.
+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`.
 -/
-structure Std.Slice.Internal.SubarrayData (α : Type u) where
+structure Subarray (α : Type u) where
   /-- The underlying array. -/
   array : Array α
   /-- The starting index of the region of interest (inclusive). -/
@@ -40,40 +42,6 @@ structure Std.Slice.Internal.SubarrayData (α : 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
 
 /--
@@ -83,8 +51,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 only [size, ge_iff_le]
+  let {array, start, stop, start_le_stop, stop_le_array_size} := s
+  simp [size]
   apply Nat.le_trans (Nat.sub_le stop start)
   assumption
 
@@ -97,7 +65,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 only [size] at this
+   simp [size] at this
    rw [Nat.add_comm]
    exact Nat.add_lt_of_lt_sub this
   s.array[s.start + i.val]
@@ -134,9 +102,7 @@ Examples:
 -/
 def popFront (s : Subarray α) : Subarray α :=
   if h : s.start < s.stop then
-    ⟨{ s.internalRepresentation with
-        start := s.start + 1,
-        start_le_stop := Nat.le_of_lt_succ (Nat.add_lt_add_right h 1) }⟩
+    { s with start := s.start + 1, start_le_stop := Nat.le_of_lt_succ (Nat.add_lt_add_right h 1) }
   else
     s
 
@@ -145,13 +111,12 @@ The empty subarray.
 
 This empty subarray is backed by an empty array.
 -/
-protected def empty : Subarray α := ⟨{
-    array := #[]
-    start := 0
-    stop := 0
-    start_le_stop := Nat.le_refl 0
-    stop_le_array_size := Nat.le_refl 0
-  }⟩
+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
 
 instance : EmptyCollection (Subarray α) :=
   ⟨Subarray.empty⟩
@@ -445,24 +410,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,11 +7,9 @@ Authors: David Thrane Christiansen
 module
 
 prelude
-public import Init.Data.Array.Basic
-public import all Init.Data.Array.Subarray
-public import Init.Omega
-
-public section
+import Init.Data.Array.Basic
+import all Init.Data.Array.Subarray
+import Init.Omega
 
 /-
 This module contains splitting operations on subarrays that crucially rely on `omega` for proof
@@ -23,24 +21,44 @@ 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 α := ⟨{
+def drop (arr : Subarray α) (i : Nat) : Subarray α where
   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 α := ⟨{
+def take (arr : Subarray α) (i : Nat) : Subarray α where
   array := arr.array
   start := arr.start
   stop := min (arr.start + i) arr.stop
@@ -50,11 +68,3 @@ def take (arr : Subarray α) (i : Nat) : Subarray α := ⟨{
   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,11 +6,9 @@ Authors: Markus Himmel
 module
 
 prelude
-public import all Init.Data.Array.Basic
-public import Init.Data.Array.Lemmas
-public import Init.Data.List.Nat.TakeDrop
-
-public section
+import all Init.Data.Array.Basic
+import Init.Data.Array.Lemmas
+import Init.Data.List.Nat.TakeDrop
 
 /-!
 These lemmas are used in the internals of HashMap.

src/Init/Data/Array/Zip.lean

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

src/Init/Data/BEq.lean

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

src/Init/Data/Basic.lean

@@ -6,15 +6,13 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Init.Data.Nat.Basic
-public import Init.Data.Fin.Basic
-public import Init.Data.List.Basic
-public import Init.Data.Char.Basic
-public import Init.Data.String.Basic
-public import Init.Data.Option.Basic
-public import Init.Data.UInt
-public import Init.Data.Repr
-public import Init.Data.ToString.Basic
-public import Init.Data.String.Extra
-
-public section
+import Init.Data.Nat.Basic
+import Init.Data.Fin.Basic
+import Init.Data.List.Basic
+import Init.Data.Char.Basic
+import Init.Data.String.Basic
+import Init.Data.Option.Basic
+import Init.Data.UInt
+import Init.Data.Repr
+import Init.Data.ToString.Basic
+import Init.Data.String.Extra

src/Init/Data/BitVec.lean

@@ -6,12 +6,10 @@ Authors: Kim Morrison
 module
 
 prelude
-public import Init.Data.BitVec.BasicAux
-public import Init.Data.BitVec.Basic
-public import Init.Data.BitVec.Bootstrap
-public import Init.Data.BitVec.Bitblast
-public import Init.Data.BitVec.Decidable
-public import Init.Data.BitVec.Lemmas
-public import Init.Data.BitVec.Folds
-
-public section
+import Init.Data.BitVec.BasicAux
+import Init.Data.BitVec.Basic
+import Init.Data.BitVec.Bootstrap
+import Init.Data.BitVec.Bitblast
+import Init.Data.BitVec.Decidable
+import Init.Data.BitVec.Lemmas
+import Init.Data.BitVec.Folds