chore: update stage0

.gitattributes

@@ -1,4 +1,3 @@
-*.lean text eol=lf
 *.expected.out -text
-RELEASES.md merge=union
+doc/changes.md merge=union
 stage0/** binary linguist-generated

.github/workflows/changelog.yml

@@ -1,33 +0,0 @@
-name: add PR to changelog
-
-on:
-  # needs read/write GH token, do *not* execute arbitrary code from PR
-  pull_request_target:
-    types: [closed]
-
-jobs:
-  update-changelog:
-    if: |
-      github.event.pull_request.merged == true &&
-      contains(github.event.pull_request.labels.*.name, 'changelog') &&
-      github.base_ref == 'master'
-    runs-on: ubuntu-latest
-    steps:
-      - uses: actions/checkout@v3
-        with:
-          # needs sufficiently elevated token to override branch protection rules
-          token: ${{ secrets.PUSH_NIGHTLY_TOKEN }}
-      - name: Update changelog
-        run: |
-          set -euxo pipefail
-          escaped_link=$(sed -e 's/[\/&]/\\&/g' <<'EOF'
-          [${{ github.event.pull_request.title}}](${{ github.event.pull_request.html_url }})
-          EOF
-          )
-          # insert link below first dashes line (https://stackoverflow.com/a/9453461/161659)
-          sed -i "0,/^---*/s/^---*/\0\n\n* $escaped_link./" RELEASES.md
-          # commit as github-actions bot (https://github.com/orgs/community/discussions/26560#discussioncomment-3252339)
-          git config user.email "41898282+github-actions[bot]@users.noreply.github.com"
-          git config user.name "github-actions[bot]"
-          git commit -i RELEASES.md -m "doc: update changelog"
-          git push

.github/workflows/ci.yml

@@ -2,45 +2,18 @@ name: CI
 on:
   push:
     branches:
-      - 'master'
+      - master
     tags:
       - '*'
   pull_request:
     branches:
       - master
   schedule:
-    - cron: '0 7 * * *'  # 8AM CET/11PM PT
-
-concurrency:
-  group: ${{ github.workflow }}-${{ github.ref }}-${{ github.event_name }}
-  cancel-in-progress: true
+    - cron: '0 0 * * *'
 
 jobs:
-  set-nightly:
-    runs-on: ubuntu-latest
-    outputs:
-      nightly: ${{ steps.set.outputs.nightly }}
-    steps:
-      - name: Checkout
-        uses: actions/checkout@v3
-        # don't schedule nightlies on forks
-        if: github.event_name == 'schedule' && github.repository == 'leanprover/lean4'
-      - name: Set Nightly
-        if: github.event_name == 'schedule' && github.repository == 'leanprover/lean4'
-        id: set
-        run: |
-          if [[ -n '${{ secrets.PUSH_NIGHTLY_TOKEN }}' ]]; then
-            git remote add nightly https://foo:'${{ secrets.PUSH_NIGHTLY_TOKEN }}'@github.com/${{ github.repository_owner }}/lean4-nightly.git
-            git fetch nightly --tags
-            LEAN_VERSION_STRING="nightly-$(date -u +%F)"
-            # do nothing if commit already has a different tag
-            if [[ $(git name-rev --name-only --tags --no-undefined HEAD 2> /dev/null || echo $LEAN_VERSION_STRING) == $LEAN_VERSION_STRING ]]; then
-              echo "nightly=$LEAN_VERSION_STRING" >> $GITHUB_OUTPUT
-            fi
-          fi
-
-  build:
-    needs: set-nightly
+  Build:
+    # don't schedule nightlies on forks
     if: github.event_name != 'schedule' || github.repository == 'leanprover/lean4'
     runs-on: ${{ matrix.os }}
     defaults:
@@ -49,16 +22,12 @@ jobs:
     strategy:
       matrix:
         include:
-          # portable release build: use channel with older glibc (2.27)
+          # portable release build: link most libraries statically and use channel with older glibc (2.27; LLVM 7)
           - name: Linux release
             os: ubuntu-latest
             release: true
-            shell: nix-shell --arg pkgsDist "import (fetchTarball \"channel:nixos-19.03\") {{}}" --run "bash -euxo pipefail {0}"
-            llvm-url: https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-linux-gnu.tar.zst
-            prepare-llvm: ../script/prepare-llvm-linux.sh lean-llvm*
-            binary-check: ldd -v
-            # foreign code may be linked against more recent glibc
-            CTEST_OPTIONS: -E 'foreign|leanlaketest_git'
+            CMAKE_OPTIONS: -DSTATIC=ON
+            shell: nix-shell --arg pkgs "import (fetchTarball \"channel:nixos-19.03\") {{}}" --argstr llvmPackages latest --run "bash -euxo pipefail {0}"
           - name: Linux
             os: ubuntu-latest
             check-stage3: true
@@ -66,51 +35,19 @@ jobs:
           - name: Linux Debug
             os: ubuntu-latest
             CMAKE_OPTIONS: -DCMAKE_BUILD_TYPE=Debug
-            # exclude seriously slow tests
-            CTEST_OPTIONS: -E 'interactivetest|leanpkgtest|laketest'
           - name: Linux fsanitize
             os: ubuntu-latest
-            # turn off custom allocator & symbolic functions to make LSAN do its magic
-            CMAKE_OPTIONS: -DLEAN_EXTRA_CXX_FLAGS=-fsanitize=address,undefined -DLEANC_EXTRA_FLAGS='-fsanitize=address,undefined -fsanitize-link-c++-runtime' -DSMALL_ALLOCATOR=OFF -DBSYMBOLIC=OFF
-            # exclude seriously slow/problematic tests (laketests crash)
-            CTEST_OPTIONS: -E 'interactivetest|leanpkgtest|laketest'
+            # turn off custom allocator to make LSAN do its magic
+            CMAKE_OPTIONS: -DLEAN_EXTRA_CXX_FLAGS=-fsanitize=address,undefined -DLEANC_EXTRA_FLAGS=-fsanitize=address,undefined -DSMALL_ALLOCATOR=OFF
           - name: macOS
             os: macos-latest
             release: true
-            shell: bash -euxo pipefail {0}
-            CMAKE_OPTIONS: -DCMAKE_OSX_DEPLOYMENT_TARGET=10.15
-            llvm-url: https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-apple-darwin.tar.zst
-            prepare-llvm: ../script/prepare-llvm-macos.sh lean-llvm*
-            binary-check: otool -L
-            tar: gtar  # https://github.com/actions/runner-images/issues/2619
-          - name: macOS aarch64
-            os: macos-latest
-            release: true
-            cross: true
-            shell: bash -euxo pipefail {0}
-            CMAKE_OPTIONS: -DCMAKE_OSX_DEPLOYMENT_TARGET=10.15 -DUSE_GMP=OFF -DLEAN_INSTALL_SUFFIX=-darwin_aarch64
-            llvm-url: https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-aarch64-apple-darwin.tar.zst https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-apple-darwin.tar.zst
-            prepare-llvm: EXTRA_FLAGS=--target=aarch64-apple-darwin ../script/prepare-llvm-macos.sh lean-llvm-aarch64-* lean-llvm-x86_64-*
-            binary-check: otool -L
-            tar: gtar  # https://github.com/actions/runner-images/issues/2619
+            CMAKE_OPTIONS: -DSTATIC=ON
           - name: Windows
-            os: windows-2022
+            os: windows-latest
             release: true
             shell: msys2 {0}
-            CMAKE_OPTIONS: -G "Unix Makefiles" -DUSE_GMP=OFF
-            # for reasons unknown, interactivetests are flaky on Windows
-            CTEST_OPTIONS: --repeat until-pass:2
-            llvm-url: https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-w64-windows-gnu.tar.zst
-            prepare-llvm: ../script/prepare-llvm-mingw.sh lean-llvm*
-            binary-check: ldd
-          - name: Linux aarch64
-            os: ubuntu-latest
-            CMAKE_OPTIONS: -DCMAKE_PREFIX_PATH=$GMP -DLEAN_INSTALL_SUFFIX=-linux_aarch64
-            release: true
-            cross: true
-            shell: nix-shell --arg pkgsDist "import (fetchTarball \"channel:nixos-19.03\") {{ localSystem.config = \"aarch64-unknown-linux-gnu\"; }}" --run "bash -euxo pipefail {0}"
-            llvm-url: https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-linux-gnu.tar.zst https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-aarch64-linux-gnu.tar.zst
-            prepare-llvm: EXTRA_FLAGS=--target=aarch64-unknown-linux-gnu ../script/prepare-llvm-linux.sh lean-llvm-aarch64-* lean-llvm-x86_64-*
+            CMAKE_OPTIONS: -G "Unix Makefiles" -DCMAKE_C_COMPILER=clang -DCMAKE_CXX_COMPILER=clang++ -DSTATIC=ON
       # complete all jobs
       fail-fast: false
     name: ${{ matrix.name }}
@@ -120,204 +57,139 @@ jobs:
       CCACHE_COMPRESS: true
       # current cache limit
       CCACHE_MAXSIZE: 200M
-      # squelch error message about missing nixpkgs channel
-      NIX_BUILD_SHELL: bash
-      LSAN_OPTIONS: max_leaks=10
-      # somehow MinGW clang64 (or cmake?) defaults to `g++` even though it doesn't exist
-      CXX: c++
     steps:
       - name: Checkout
-        uses: actions/checkout@v3
+        uses: actions/checkout@v2
         with:
-          submodules: true
+          # interferes with lean4-nightly authentication
+          persist-credentials: false
       - name: Install Nix
-        uses: cachix/install-nix-action@v18
+        uses: cachix/install-nix-action@v12
         with:
-          install_url: https://releases.nixos.org/nix/nix-2.12.0/install
-        if: matrix.os == 'ubuntu-latest'
+          # used only for providing a more recent `bash` on macOS
+          nix_path: nixpkgs=channel:nixos-unstable
+        if: matrix.os != 'windows-latest'
       - name: Install MSYS2
         uses: msys2/setup-msys2@v2
         with:
-          msystem: clang64
-          # `:p` means prefix with appropriate msystem prefix
-          pacboy: "make python cmake:p clang:p ccache:p gmp:p git zip unzip diffutils binutils tree zstd:p tar"
-        if: matrix.os == 'windows-2022'
-      - name: Install Brew Packages
-        run: |
-          brew install ccache tree zstd coreutils gmp
-        if: matrix.os == 'macos-latest'
+          install: make python mingw-w64-x86_64-cmake mingw-w64-x86_64-clang mingw-w64-x86_64-ccache git diffutils
+        if: matrix.os == 'windows-latest'
       - name: Cache
-        uses: actions/cache@v3
+        uses: actions/cache@v2
         with:
           path: .ccache
-          key: ${{ matrix.name }}-build-v3-${{ github.sha }}
+          key: ${{ matrix.name }}-build-${{ github.sha }}
           # fall back to (latest) previous cache
           restore-keys: |
-            ${{ matrix.name }}-build-v3
+            ${{ matrix.name }}-build
       - name: Setup
         run: |
           # open nix-shell once for initial setup
           true
-        if: matrix.os == 'ubuntu-latest'
-      - name: Set up core dumps
-        run: |
-          mkdir -p $PWD/coredumps
-          # store in current directory, for easy uploading together with binary
-          echo $PWD/coredumps/%e.%p.%t | sudo tee /proc/sys/kernel/core_pattern
-        if: matrix.os == 'ubuntu-latest'
+        if: matrix.os != 'windows-latest'
+      # remove problematic tests for sanitized build
+      - name: Pre build
+        run: rm tests/compiler/StackOverflow.lean tests/compiler/StackOverflowTask.lean
+        if: matrix.name == 'Linux fsanitize'
       - name: Build
         run: |
           mkdir build
           cd build
-          ulimit -c unlimited # coredumps
-          OPTIONS=()
-          if [[ -n '${{ matrix.prepare-llvm }}' ]]; then
-            wget -q ${{ matrix.llvm-url }}
-            PREPARE="$(${{ matrix.prepare-llvm }})"
-            eval "OPTIONS+=($PREPARE)"
+          OPTIONS=
+          if [[ $GITHUB_EVENT_NAME == 'schedule' && -n '${{ matrix.release }}' && -n '${{ secrets.PUSH_NIGHTLY_TOKEN }}' ]]; then
+            git remote add nightly https://foo:'${{ secrets.PUSH_NIGHTLY_TOKEN }}'@github.com/${{ github.repository_owner }}/lean4-nightly.git
+            git fetch nightly --tags
+            LEAN_VERSION_STRING="nightly-$(date -u +%F)"
+            # do nothing if commit already has a different tag
+            if [[ $(git name-rev --name-only --tags --no-undefined HEAD 2> /dev/null || echo $LEAN_VERSION_STRING) == $LEAN_VERSION_STRING ]]; then
+              OPTIONS=-DLEAN_SPECIAL_VERSION_DESC=$LEAN_VERSION_STRING
+              echo "LEAN_VERSION_STRING=$LEAN_VERSION_STRING" >> $GITHUB_ENV
+            fi
           fi
-          if [[ -n '${{ matrix.release }}' && -n '${{ needs.set-nightly.outputs.nightly }}' ]]; then
-            OPTIONS+=(-DLEAN_SPECIAL_VERSION_DESC=${{ needs.set-nightly.outputs.nightly }})
-          fi
-          # contortion to support empty OPTIONS with old macOS bash
-          cmake .. ${{ matrix.CMAKE_OPTIONS }} ${OPTIONS[@]+"${OPTIONS[@]}"} -DLEAN_INSTALL_PREFIX=$PWD/..
+          cmake .. ${{ matrix.CMAKE_OPTIONS }} $OPTIONS
           make -j4
-          make install
-      - name: Check Binaries
-        run: ${{ matrix.binary-check }} lean-*/bin/* || true
-      - name: List Install Tree
+      # de-Nix-ify binaries
+      - name: Patch
         run: |
-          # omit contents of Init/, ...
-          tree --du -h lean-* | grep -E ' (Init|Lean|Lake|LICENSE|[a-z])'
+          for f in lean leanpkg; do
+            patchelf --set-interpreter /lib64/ld-linux-x86-64.so.2 --remove-rpath build/stage1/bin/$f
+          done
+        if: matrix.name == 'Linux release'
+      - name: Patch
+        run: |
+          for f in lean leanpkg; do
+            for lib in $(otool -L build/stage1/bin/$f | tail -n +2 | cut -d' ' -f1); do
+              install_name_tool -change "$lib" "/usr/lib/$(basename $lib | sed 's/libc++\.1\.0/libc++.1/')" build/stage1/bin/$f
+            done
+          done
+        if: matrix.name == 'macOS'
       - name: Pack
-        run: |
-          dir=$(echo lean-*)
-          mkdir pack
-          # high-compression tar.zst + zip for release, fast tar.zst otherwise
-          if [[ '${{ startsWith(github.ref, 'refs/tags/') && matrix.release }}' == true || -n '${{ needs.set-nightly.outputs.nightly }}' ]]; then
-            ${{ matrix.tar || 'tar' }} cf - $dir | zstd -T0 --no-progress -19 -o pack/$dir.tar.zst
-            zip -rq pack/$dir.zip $dir
-          else
-            ${{ matrix.tar || 'tar' }} cf - $dir | zstd -T0 --no-progress -o pack/$dir.tar.zst
-          fi
-      - uses: actions/upload-artifact@v3
-        if: matrix.release
+        run: cd build/stage1; cpack
+      - uses: actions/upload-artifact@v2
         with:
           name: build-${{ matrix.name }}
-          path: pack/*
-      - name: Lean stats
-        run: |
-          build/stage1/bin/lean --stats src/Lean.lean
-        if: ${{ !matrix.cross }}
+          path: build/stage1/lean-*
       - name: Test
         run: |
           cd build/stage1
-          ulimit -c unlimited # coredumps
-          # exclude nonreproducible test
-          ctest -j4 --output-on-failure -E leanlaketest_git ${{ matrix.CTEST_OPTIONS }} < /dev/null
-        if: ${{ !matrix.cross }}
-      - name: Check Test Binary
-        run: ${{ matrix.binary-check }} tests/compiler/534.lean.out
-        if: ${{ !matrix.cross }}
+          ctest -j4 --output-on-failure < /dev/null
       - name: Build Stage 2
         run: |
           cd build
-          ulimit -c unlimited # coredumps
           make -j4 stage2
         if: matrix.build-stage2 || matrix.check-stage3
       - name: Check Stage 3
         run: |
           cd build
-          ulimit -c unlimited # coredumps
           make -j4 check-stage3
         if: matrix.check-stage3
       - name: Test Speedcenter Benchmarks
         run: |
           echo -1 | sudo tee /proc/sys/kernel/perf_event_paranoid
           export BUILD=$PWD/build PATH=$PWD/build/stage1/bin:$PATH
-          cd tests/bench
-          nix shell .#temci -c temci exec --config speedcenter.yaml --included_blocks fast --runs 1
+          cd tests/bench; temci exec --config speedcenter.yaml --included_blocks fast --runs 1
         if: matrix.test-speedcenter
       - name: Check rebootstrap
         run: |
           cd build
-          ulimit -c unlimited # coredumps
           make update-stage0 && make -j4
         if: matrix.name == 'Linux'
       - name: CCache stats
         run: ccache -s
-      - name: Show stacktrace for coredumps
-        if: ${{ failure() }} && matrix.os == 'ubuntu-latest'
-        run: |
-          for c in coredumps/*; do
-            progbin="$(file $c | sed "s/.*execfn: '\([^']*\)'.*/\1/")"
-            echo bt | $GDB/bin/gdb -q $progbin $c || true
-          done
-      - name: Upload coredumps
-        uses: actions/upload-artifact@v3
-        if: ${{ failure() }} && matrix.os == 'ubuntu-latest'
-        with:
-          name: coredumps-${{ matrix.name }}
-          path: |
-            ./coredumps
-            ./build/stage0/bin/lean
-            ./build/stage0/lib/lean/libleanshared.so
-            ./build/stage1/bin/lean
-            ./build/stage1/lib/lean/libleanshared.so
-            ./build/stage2/bin/lean
-            ./build/stage2/lib/lean/libleanshared.so
-
-  release:
-    if: startsWith(github.ref, 'refs/tags/')
-    runs-on: ubuntu-latest
-    needs: build
-    steps:
-      - uses: actions/download-artifact@v3
-        with:
-          path: artifacts
       - name: Release
         uses: softprops/action-gh-release@v1
+        if: ${{ startsWith(github.ref, 'refs/tags/v') && matrix.release }}
         with:
-          files: artifacts/*/*
-          fail_on_unmatched_files: true
+          files: build/stage1/lean-*
         env:
           GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
-
-  release-nightly:
-    needs: [set-nightly, build]
-    if: needs.set-nightly.outputs.nightly
-    runs-on: ubuntu-latest
-    steps:
-      - name: Checkout
-        uses: actions/checkout@v3
-        with:
-          # needed for tagging
-          fetch-depth: 0
-          token: ${{ secrets.PUSH_NIGHTLY_TOKEN }}
-      - uses: actions/download-artifact@v3
-        with:
-          path: artifacts
       - name: Prepare Nightly Release
+        if: env.LEAN_VERSION_STRING
         run: |
-          git remote add nightly https://foo:'${{ secrets.PUSH_NIGHTLY_TOKEN }}'@github.com/${{ github.repository_owner }}/lean4-nightly.git
+          # can't push shallow checkout
+          git fetch --unshallow
           git fetch nightly --tags
-          git tag ${{ needs.set-nightly.outputs.nightly }}
-          git push nightly ${{ needs.set-nightly.outputs.nightly }}
-          last_tag=$(git describe HEAD^ --abbrev=0 --tags)
-          echo -e "*Changes since ${last_tag}:*\n\n" > diff.md
-          git show $last_tag:RELEASES.md > old.md
-          #./script/diff_changelogs.py old.md doc/changes.md >> diff.md
-          diff --changed-group-format='%>' --unchanged-group-format='' old.md RELEASES.md >> diff.md || true
-          echo -e "\n*Full commit log*\n" >> diff.md
-          git log --oneline $last_tag..HEAD | sed 's/^/* /' >> diff.md
+          if git tag $LEAN_VERSION_STRING && git push nightly $LEAN_VERSION_STRING; then
+            last_tag=$(git describe HEAD^ --abbrev=0 --tags)
+            echo -e "Changes since ${last_tag}:\n\n" > diff.md
+            #git show $last_tag:doc/changes.md > old.md
+            #./script/diff_changelogs.py old.md doc/changes.md >> diff.md
+            echo -e "*Full commit log*\n" >> diff.md
+            git log --oneline $last_tag..HEAD | sed 's/^/* /' >> diff.md
+          else
+            # make sure every runner is building the same commit
+            [ $(git rev-parse HEAD) == $(git rev-parse $LEAN_VERSION_STRING) ] || exit 11
+            echo -n > diff.md
+          fi
       - name: Release Nightly
-        uses: softprops/action-gh-release@v1
+        # need unreleased version for fixed `repository`
+        uses: Kha/action-gh-release@master
+        if: env.LEAN_VERSION_STRING
         with:
           body_path: diff.md
           prerelease: true
-          files: artifacts/*/*
-          fail_on_unmatched_files: true
-          tag_name: ${{ needs.set-nightly.outputs.nightly }}
+          files: build/stage1/lean-*
+          tag_name: ${{ env.LEAN_VERSION_STRING }}
           repository: ${{ github.repository_owner }}/lean4-nightly
         env:
           GITHUB_TOKEN: ${{ secrets.PUSH_NIGHTLY_TOKEN }}

.github/workflows/nix-ci.yml

@@ -9,23 +9,23 @@ on:
     branches:
       - master
 
-concurrency:
-  group: ${{ github.workflow }}-${{ github.ref }}
-  cancel-in-progress: true
-
 jobs:
   Build:
     runs-on: ${{ matrix.os }}
     defaults:
       run:
+        # Can't use `nix-shell` without configured nixpkgs path on macOS
         shell: nix -v --experimental-features "nix-command flakes" run .#ciShell -- bash -euxo pipefail {0}
     strategy:
       matrix:
         include:
-          - name: Nix Linux
+          - name: Linux
             os: ubuntu-latest
-          #- name: Nix macOS
-          #  os: macos-latest
+            # latest builds on https://hydra.nixos.org/jobset/nix/master/all at the time
+            nix_url: https://hydra.nixos.org/build/135773533/download/1/nix-2.4pre20210125_36c4d6f-x86_64-linux.tar.xz
+          - name: macOS
+            os: macos-latest
+            nix_url: https://hydra.nixos.org/build/135773542/download/1/nix-2.4pre20210125_36c4d6f-x86_64-darwin.tar.xz
       # complete all jobs
       fail-fast: false
     name: ${{ matrix.name }}
@@ -33,79 +33,70 @@ jobs:
       NIX_BUILD_ARGS: -v --print-build-logs --fallback
     steps:
       - name: Checkout
-        uses: actions/checkout@v3
+        uses: actions/checkout@v2
+      # Install flakes-enabled Nix manually from Hydra since `install-nix-action` doesn't accept raw tarballs
       - name: Install Nix
-        uses: cachix/install-nix-action@v18
-        with:
-          # https://github.com/NixOS/nix/issues/6572
-          install_url: https://releases.nixos.org/nix/nix-2.7.0/install
-          extra_nix_config: |
+        shell: bash -euo pipefail {0}
+        run: |
+          curl ${{ matrix.nix_url }} | tar -xJ
+          # Do a single-user install so actions/cache doesn't get confused about permissions
+          nix-*/install --no-daemon --no-channel-add --darwin-use-unencrypted-nix-store-volume
+          rm -rf nix-*
+      # Call `install-nix-action` anyways to run its Actions-specific setup
+      - name: Setup Nix
+        uses: cachix/install-nix-action@v12
+      - name: Fixup install-nix-action
+        shell: bash -euo pipefail {0}
+        run: |
+          # the path set by install-nix-action is valid only for multi-user installations
+          echo "NIX_SSL_CERT_FILE=$HOME/.nix-profile/etc/ssl/certs/ca-bundle.crt" > $GITHUB_ENV
+        if: matrix.name == 'macOS'
+      - name: Further setup Nix
+        run: |
+          mkdir -p ~/.config/nix
+          echo '
+            max-jobs = auto
             extra-sandbox-paths = /nix/var/cache/ccache
-            substituters = file://${{ github.workspace }}/nix-store-cache-copy?priority=10&trusted=true https://cache.nixos.org
-      - name: Set Up Nix Cache
-        uses: actions/cache@v3
-        with:
-          path: nix-store-cache
-          key: ${{ matrix.name }}-nix-store-cache-${{ github.sha }}
-          # fall back to (latest) previous cache
-          restore-keys: |
-            ${{ matrix.name }}-nix-store-cache
-      - name: Further Set Up Nix Cache
-        shell: bash -euxo pipefail {0}
-        run: |
-          # Nix seems to mutate the cache, so make a copy
-          cp -r nix-store-cache nix-store-cache-copy || true
-      - name: Prepare CCache Cache
-        shell: bash -euxo pipefail {0}
-        run: |
+            extra-trusted-substituters = https://lean4.cachix.org/
+            extra-trusted-public-keys = lean4.cachix.org-1:mawtxSxcaiWE24xCXXgh3qnvlTkyU7evRRnGeAhD4Wk=' > ~/.config/nix/nix.conf
           sudo mkdir -m0770 -p /nix/var/cache/ccache
-          sudo chown -R $USER /nix/var/cache/ccache
+          # macOS standard chown doesn't support --reference
+          nix shell .#nixpkgs.coreutils -c sudo chown --reference=/nix /nix/var/cache/ccache
+          echo 'max_size = 50M' > /nix/var/cache/ccache/ccache.conf
+
+          # install & use Cachix manually since `cachix-action` pushes *all* derivations (incl. `$mod-deps`, stage 2&3, etc.)
+          nix-env -iA cachix -f https://cachix.org/api/v1/install
       - name: Setup CCache Cache
-        uses: actions/cache@v3
+        uses: actions/cache@v2
         with:
           path: /nix/var/cache/ccache
           key: ${{ matrix.name }}-nix-ccache-${{ github.sha }}
           # fall back to (latest) previous cache
           restore-keys: |
             ${{ matrix.name }}-nix-ccache
-      - name: Further Set Up CCache Cache
-        shell: bash -euxo pipefail {0}
-        run: |
-          sudo chown -R root:nixbld /nix/var/cache
-          sudo chmod -R 770 /nix/var/cache
-      - name: Install Cachix
-        uses: cachix/cachix-action@v12
-        with:
-          name: lean4
-          authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}'
-          skipPush: true  # we push specific outputs only
       - name: Build
         run: |
-          nix build $NIX_BUILD_ARGS .#cacheRoots -o push-build
+          # .o files are not a runtime dependency on macOS because of lack of thin archives
+          nix build $NIX_BUILD_ARGS .#stage0 .#stage1.lean-all .#Lean.oTree -o push-build
       - name: Test
         run: |
           nix build $NIX_BUILD_ARGS .#test -o push-test
       - name: Build manual
         run: |
-          nix build $NIX_BUILD_ARGS --update-input lean --no-write-lock-file ./doc#{lean-mdbook,leanInk,alectryon,test,inked} -o push-doc
-          nix build $NIX_BUILD_ARGS --update-input lean --no-write-lock-file ./doc
-        if: matrix.name == 'Nix Linux'
+          nix build $NIX_BUILD_ARGS .#mdbook .#doc-test -o push-doc
+          nix build $NIX_BUILD_ARGS .#doc
+        if: matrix.name == 'Linux'
       - name: Push to Cachix
         run: |
-          [ -z "${{ secrets.CACHIX_AUTH_TOKEN }}" ] || cachix push -j4 lean4 ./push-* || true
-      - name: Rebuild Nix Store Cache
-        run: |
-          rm -rf nix-store-cache || true
-          nix copy ./push-* --to file://$PWD/nix-store-cache?compression=none
+          [ -z "$CACHIX_AUTH_TOKEN" ] || cachix push -j4 lean4 ./push-* || true
+        env:
+          CACHIX_AUTH_TOKEN: '${{ secrets.CACHIX_AUTH_TOKEN }}'
       - name: Publish manual
         uses: peaceiris/actions-gh-pages@v3
         with:
           github_token: ${{ secrets.GITHUB_TOKEN }}
           publish_dir: ./result
           destination_dir: ./doc
-        if: matrix.name == 'Nix Linux' && github.ref == 'refs/heads/master' && github.event_name == 'push'
-      - name: Fixup CCache Cache
-        run: |
-          sudo chown -R $USER /nix/var/cache
+        if: matrix.name == 'Linux' && github.ref == 'refs/heads/master' && github.event_name == 'push'
       - name: CCache stats
         run: CCACHE_DIR=/nix/var/cache/ccache nix run .#nixpkgs.ccache -- -s

.github/workflows/pr.yml

@@ -1,31 +0,0 @@
-name: sanity-check opened PRs
-
-on:
-  # needs read/write GH token, do *not* execute arbitrary code from PR
-  pull_request_target:
-    types: [opened]
-
-jobs:
-  check-pr:
-    runs-on: ubuntu-latest
-    steps:
-      - name: Check Commit Message
-        uses: actions/github-script@v6
-        with:
-          github-token: ${{ secrets.GITHUB_TOKEN }}
-          script: |
-            const { data: commits } = await github.rest.pulls.listCommits({
-              owner: context.repo.owner,
-              repo: context.repo.repo,
-              pull_number: context.issue.number,
-            });
-            console.log(commits[0].commit.message);
-            // check first commit only (and only once) since later commits might be intended to be squashed away
-            if (!/^(feat|fix|doc|style|refactor|test|chore|perf): .*[^.]($|\n\n)/.test(commits[0].commit.message)) {
-              await github.rest.issues.createComment({
-                owner: context.repo.owner,
-                repo: context.repo.repo,
-                issue_number: context.issue.number,
-                body: 'Thanks for your contribution! Please make sure to follow our [Commit Convention](https://leanprover.github.io/lean4/doc/dev/commit_convention.html).',
-              });
-            }

.gitignore

@@ -21,8 +21,3 @@ settings.json
 CMakeSettings.json
 CppProperties.json
 result
-fwIn.txt
-fwOut.txt
-wdErr.txt
-wdIn.txt
-wdOut.txt

.gitmodules

@@ -1,4 +0,0 @@
-[submodule "lake"]
-        path = src/lake
-        url = https://github.com/leanprover/lake.git
-        ignore = untracked

.ignore

@@ -1 +0,0 @@
-stage0/

.vscode/settings.json

@@ -1,7 +1,3 @@
 {
-    "files.insertFinalNewline": true,
-    "files.trimTrailingWhitespace": true,
-    "[markdown]": {
-        "rewrap.wrappingColumn": 70
-    }
+    "files.insertFinalNewline": true
 }

CMakeLists.txt

@@ -2,20 +2,13 @@ cmake_minimum_required(VERSION 3.11)
 # store all variables passed on the command line into CL_ARGS so we can pass them to the stage builds
 # https://stackoverflow.com/a/48555098/161659
 # MUST be done before call to 'project'
-# Use standard release build (discarding LEAN_CXX_EXTRA_FLAGS etc.) for stage0 by default since it is assumed to be "good", but still pass through CMake platform arguments (compiler, toolchain file, ..).
-# Use `STAGE0_` prefix to pass variables to stage0 explicitly.
 get_cmake_property(vars CACHE_VARIABLES)
 foreach(var ${vars})
   get_property(currentHelpString CACHE "${var}" PROPERTY HELPSTRING)
-  if("${var}" MATCHES "STAGE0_(.*)")
-    list(APPEND STAGE0_ARGS "-D${CMAKE_MATCH_1}=${${var}}")
-  elseif("${currentHelpString}" MATCHES "No help, variable specified on the command line." OR "${currentHelpString}" STREQUAL "")
+  if("${currentHelpString}" MATCHES "No help, variable specified on the command line." OR "${currentHelpString}" STREQUAL "")
     list(APPEND CL_ARGS "-D${var}=${${var}}")
-    if("${var}" STREQUAL "USE_GMP")
-      # must forward options that generate incompatible .olean format
-      list(APPEND STAGE0_ARGS "-D${var}=${${var}}")
-    endif()
-  elseif(("${var}" MATCHES "CMAKE_.*") AND NOT ("${var}" MATCHES "CMAKE_BUILD_TYPE") AND NOT ("${var}" MATCHES "CMAKE_HOME_DIRECTORY"))
+  endif()
+  if(("${var}" MATCHES "CMAKE_.*") AND NOT ("${var}" MATCHES "CMAKE_BUILD_TYPE") AND NOT ("${var}" MATCHES "CMAKE_HOME_DIRECTORY"))
     list(APPEND PLATFORM_ARGS "-D${var}=${${var}}")
   endif()
 endforeach()
@@ -44,8 +37,9 @@ ExternalProject_add(stage0
   SOURCE_DIR "${LEAN_SOURCE_DIR}/stage0"
   SOURCE_SUBDIR src
   BINARY_DIR stage0
+  # always use standard release build (discarding LEAN_CXX_EXTRA_FLAGS etc.) for stage0 since it is assumed to be "good", but still pass through CMake platform arguments (compiler, toolchain file, ..)
   # do not rebuild stage0 when git hash changes; it's not from this commit anyway
-  CMAKE_ARGS -DSTAGE=0 -DUSE_GITHASH=OFF ${PLATFORM_ARGS} ${STAGE0_ARGS}
+  CMAKE_ARGS -DSTAGE=0 -DCMAKE_BUILD_TYPE=Release -DUSE_GITHASH=OFF ${PLATFORM_ARGS}
   BUILD_ALWAYS ON  # cmake doesn't auto-detect changes without a download method
   INSTALL_COMMAND ""  # skip install
   DEPENDS ${EXTRA_DEPENDS}
@@ -63,7 +57,8 @@ ExternalProject_add(stage2
   SOURCE_DIR "${LEAN_SOURCE_DIR}"
   SOURCE_SUBDIR src
   BINARY_DIR stage2
-  CMAKE_ARGS -DSTAGE=2 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage1 ${CL_ARGS}
+  # reuse libleancpp.a, which doesn't change
+  CMAKE_ARGS -DSTAGE=2 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage1 -DLEANCPP="${CMAKE_BINARY_DIR}/stage1/lib/lean/libleancpp.a" ${CL_ARGS}
   BUILD_ALWAYS ON
   INSTALL_COMMAND ""
   DEPENDS stage1
@@ -73,7 +68,7 @@ ExternalProject_add(stage3
   SOURCE_DIR "${LEAN_SOURCE_DIR}"
   SOURCE_SUBDIR src
   BINARY_DIR stage3
-  CMAKE_ARGS -DSTAGE=3 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage2 ${CL_ARGS}
+  CMAKE_ARGS -DSTAGE=3 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage2 -DLEANCPP="${CMAKE_BINARY_DIR}/stage1/lib/lean/libleancpp.a" ${CL_ARGS}
   BUILD_ALWAYS ON
   INSTALL_COMMAND ""
   DEPENDS stage2

CONTRIBUTING.md

@@ -15,10 +15,6 @@ community using the [lean4 Zulip channel](https://leanprover.zulipchat.com/#narr
 
 Simple fixes for **typos and clear bugs** are welcome.
 
-# **IMPORTANT**
-
-We are currently overwhelmed. We respectfully request that you hold off on submitting Pull Requests and creating Request for Comments (RFCs) at this time. Our team is actively seeking funding to expand the Lean development team and improve our capacity to review and integrate contributions. We appreciate your understanding and look forward to being able to accept contributions in the near future. In the meantime, the process described in the following sections is temporarily suspended.
-
 ## Documentation
 
 Tutorial-like examples are very welcome.
@@ -54,8 +50,8 @@ We don't want to waste your time by you implementing a feature and then us not b
 
 ## How to Contribute
 
-* Always follow the [commit convention](https://leanprover.github.io/lean4/doc/dev/commit_convention.html).
+* Always follow the [commit convention](https://leanprover.github.io/lean4/doc/commit_convention.html).
 * Follow the style of the surrounding code. When in doubt, look at other files using the particular syntax as well.
 * Make sure your code is documented.
 * New features or bug fixes should come with appropriate tests.
-* Ensure all tests work before submitting a PR; see [Development Setup](https://leanprover.github.io/lean4/doc/make/index.html#development-setup) and [Fixing Tests](https://leanprover.github.io/lean4/doc/dev/fixing_tests.html).
+* Ensure all tests work before submitting a PR; see [Development Setup](https://leanprover.github.io/lean4/doc/make/index.html#development-setup) and [Fixing Tests](https://leanprover.github.io/lean4/doc/fixing_tests.html).

README.md

@@ -3,15 +3,8 @@ This is the repository for **Lean 4**, which is currently being released as mile
 
 # About
 
-- [Quickstart](https://github.com/leanprover/lean4/blob/master/doc/quickstart.md)
-- [Walkthrough installation video](https://www.youtube.com/watch?v=yZo6k48L0VY)
-- [Quick tour video](https://youtu.be/zyXtbb_eYbY)
 - [Homepage](https://leanprover.github.io)
-- [Theorem Proving Tutorial](https://leanprover.github.io/theorem_proving_in_lean4/)
-- [Functional Programming in Lean](https://leanprover.github.io/functional_programming_in_lean/)
 - [Manual](https://leanprover.github.io/lean4/doc/)
-- [Release notes](RELEASES.md) starting at v4.0.0-m3
-- [Examples](https://leanprover.github.io/lean4/doc/examples.html)
 - [FAQ](https://leanprover.github.io/lean4/doc/faq.html)
 
 # Installation

doc/BoolExpr.lean

@@ -1,3 +1,4 @@
+import Std
 open Std
 open Lean
 
@@ -103,9 +104,9 @@ syntax entry := ident " ↦ " term:max
 syntax entry,* "⊢" term : term
 
 macro_rules
-  | `( $[$xs ↦ $vs],* ⊢ $p) =>
+  | `( $[$xs:ident ↦ $vs:term],* ⊢ $p:term ) =>
     let xs := xs.map fun x => quote x.getId.toString
-    `(denote (List.toAssocList [$[($xs, $vs)],*]) `[BExpr| $p])
+    `(denote (List.toAssocList [$[( $xs , $vs )],*]) `[BExpr| $p])
 
 #check b ↦ true ⊢ b ∨ b
 #eval  a ↦ false, b ↦ false ⊢ b ∨ a

doc/SUMMARY.md

@@ -2,44 +2,22 @@
 
 - [What is Lean](./whatIsLean.md)
 - [Tour of Lean](./tour.md)
-- [Setting Up Lean](./quickstart.md)
-  - [Extended Setup Notes](./setup.md)
-- [Theorem Proving in Lean](./tpil.md)
-- [Functional Programming in Lean](fplean.md)
-- [Examples](./examples.md)
-  - [Palindromes](examples/palindromes.lean.md)
-  - [Binary Search Trees](examples/bintree.lean.md)
-  - [A Certified Type Checker](examples/tc.lean.md)
-  - [The Well-Typed Interpreter](examples/interp.lean.md)
-  - [Dependent de Bruijn Indices](examples/deBruijn.lean.md)
-  - [Parametric Higher-Order Abstract Syntax](examples/phoas.lean.md)
+- [Setting Up Lean](./setup.md)
+  - [Quickstart](./quickstart.md)
 
 # Language Manual
-<!-- - [Using Lean](./using_lean.md) -->
-<!-- - [Lexical Structure](./lexical_structure.md) -->
-<!-- - [Expressions](./expressions.md) -->
-<!-- - [Declarations](./declarations.md) -->
+
+- [Dependent Types](./deptypes.md)
+  - [Simple Type Theory](./simptypes.md)
+  - [Types as objects](./typeobjs.md)
+  - [Function Abstraction and Evaluation](./funabst.md)
+  - [Introducing Definitions](./introdef.md)
+  - [What makes dependent type theory dependent?](./dep.md)
 - [Organizational features](./organization.md)
   - [Sections](./sections.md)
   - [Namespaces](./namespaces.md)
   - [Implicit Arguments](./implicit.md)
   - [Auto Bound Implicit Arguments](./autobound.md)
-<!-- - [Dependent Types](./deptypes.md) -->
-<!--   - [Simple Type Theory](./simptypes.md) -->
-<!--   - [Types as objects](./typeobjs.md) -->
-<!--   - [Function Abstraction and Evaluation](./funabst.md) -->
-<!--   - [Introducing Definitions](./introdef.md) -->
-<!--   - [What makes dependent type theory dependent?](./dep.md) -->
-<!-- - [Tactics](./tactics.md) -->
-- [Syntax Extensions](./syntax.md)
-  - [The `do` Notation](./do.md)
-  - [String Interpolation](./stringinterp.md)
-  - [User-Defined Notation](./notation.md)
-  - [Macro Overview](./macro_overview.md)
-  - [Elaborators](./elaborators.md)
-  - [Examples](./syntax_examples.md)
-    - [Balanced Parentheses](./syntax_example.md)
-    - [Arithmetic DSL](./metaprogramming-arith.md)
 - [Declaring New Types](./decltypes.md)
   - [Enumerated Types](./enum.md)
   - [Inductive Types](./inductive.md)
@@ -59,36 +37,25 @@
   - [Thunk](./thunk.md)
   - [Task and Thread](./task.md)
 - [Functions](./functions.md)
-- [Monads](./monads/intro.md)
-  - [Functor](./monads/functors.lean.md)
-  - [Applicative](./monads/applicatives.lean.md)
-  - [Monad](./monads/monads.lean.md)
-  - [Reader](./monads/readers.lean.md)
-  - [State](./monads/states.lean.md)
-  - [Except](./monads/except.lean.md)
-  - [Transformers](./monads/transformers.lean.md)
-  - [Laws](./monads/laws.lean.md)
+- [Tactics](./tactics.md)
+- [Syntax Extensions](./syntax.md)
+  - [The `do` Notation](./do.md)
+  - [String Interpolation](./stringinterp.md)
 
 # Other
 
 - [Frequently Asked Questions](./faq.md)
 - [Significant Changes from Lean 3](./lean3changes.md)
 - [Syntax Highlighting Lean in LaTeX](./syntax_highlight_in_latex.md)
-- [User Widgets](examples/widgets.lean.md)
-- [Semantic Highlighting](./semantic_highlighting.md)
 
 # Development
 
-- [Development Guide](./dev/index.md)
+- [Commit Convention](./commit_convention.md)
 - [Building Lean](./make/index.md)
-  - [Ubuntu Setup](./make/ubuntu.md)
+  - [Ubuntu Setup](./make/ubuntu-16.04.md)
   - [macOS Setup](./make/osx-10.9.md)
-  - [Windows MSYS2 Setup](./make/msys2.md)
-  - [Windows with WSL](./make/wsl.md)
+  - [Windows Setup](./make/msys2.md)
   - [Nix Setup (*Experimental*)](./make/nix.md)
-- [Bootstrapping](./dev/bootstrap.md)
-- [Testing](./dev/testing.md)
-- [Debugging](./dev/debugging.md)
-- [Commit Convention](./dev/commit_convention.md)
-- [Building This Manual](./dev/mdbook.md)
-- [Foreign Function Interface](./dev/ffi.md)
+- [Building This Manual](./mdbook.md)
+- [Fixing Tests](./fixing_tests.md)
+- [Debugging](./debugging.md)

doc/alectryon.css

@@ -1,786 +0,0 @@
-@charset "UTF-8";
-/*
-Copyright © 2019 Clément Pit-Claudel
-
-Permission is hereby granted, free of charge, to any person obtaining a copy
-of this software and associated documentation files (the "Software"), to deal
-in the Software without restriction, including without limitation the rights
-to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
-copies of the Software, and to permit persons to whom the Software is
-furnished to do so, subject to the following conditions:
-
-The above copyright notice and this permission notice shall be included in all
-copies or substantial portions of the Software.
-
-THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
-IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
-FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
-AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
-LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
-OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
-SOFTWARE.
-*/
-
-/*******************************/
-/* CSS reset for .alectryon-io */
-/*******************************/
-
-.content {
-    /*
-    Use `initial` instead of `contents` to avoid a browser bug which removes
-    the element from the accessibility tree.
-    https://developer.mozilla.org/en-US/docs/Web/CSS/display#display_contents
-     */
-    display: initial;
-}
-
-.alectryon-io blockquote {
-    line-height: inherit;
-}
-
-.alectryon-io blockquote:after {
-    display: none;
-}
-
-.alectryon-io label {
-    display: inline;
-    font-size: inherit;
-    margin: 0;
-}
-
-.alectryon-io a {
-    text-decoration: none !important;
-    font-style: oblique !important;
-    color: unset;
-}
-
-/* Undo <small> and <blockquote>, added to improve RSS rendering. */
-
-.alectryon-io small.alectryon-output,
-.alectryon-io small.alectryon-type-info {
-    font-size: inherit;
-}
-
-.alectryon-io blockquote.alectryon-goal,
-.alectryon-io blockquote.alectryon-message {
-    font-weight: normal;
-    font-size: inherit;
-}
-
-/***************/
-/* Main styles */
-/***************/
-
-.alectryon-coqdoc .doc .code,
-.alectryon-coqdoc .doc .comment,
-.alectryon-coqdoc .doc .inlinecode,
-.alectryon-mref,
-.alectryon-block, .alectryon-io,
-.alectryon-toggle-label, .alectryon-banner {
-    font-family: "Source Code Pro", Consolas, "Ubuntu Mono", Menlo, "DejaVu Sans Mono", monospace, monospace !important;
-    font-size: 0.875em;
-    font-feature-settings: "COQX" 1 /* Coq ligatures */, "XV00" 1 /* Legacy */, "calt" 1 /* Fallback */;
-    line-height: initial;
-}
-
-.alectryon-io, .alectryon-block, .alectryon-toggle-label, .alectryon-banner {
-    overflow: visible;
-    overflow-wrap: break-word;
-    position: relative;
-    white-space: pre-wrap;
-}
-
-/*
-CoqIDE doesn't turn off the unicode bidirectional algorithm (and PG simply
-respects the user's `bidi-display-reordering` setting), so don't turn it off
-here either.  But beware unexpected results like `Definition test_אב := 0.`
-
-.alectryon-io span {
-    direction: ltr;
-    unicode-bidi: bidi-override;
-}
-
-In any case, make an exception for comments:
-
-.highlight .c {
-    direction: embed;
-    unicode-bidi: initial;
-}
-*/
-
-.alectryon-mref,
-.alectryon-mref-marker {
-    align-self: center;
-    box-sizing: border-box;
-    display: inline-block;
-    font-size: 80%;
-    font-weight: bold;
-    line-height: 1;
-    box-shadow: 0 0 0 1pt black;
-    padding: 1pt 0.3em;
-    text-decoration: none;
-}
-
-.alectryon-block .alectryon-mref-marker,
-.alectryon-io .alectryon-mref-marker {
-    user-select: none;
-    margin: -0.25em 0 -0.25em 0.5em;
-}
-
-.alectryon-inline .alectryon-mref-marker {
-    margin: -0.25em 0.15em -0.25em 0.625em; /* 625 = 0.5em / 80% */
-}
-
-.alectryon-mref {
-    color: inherit;
-    margin: -0.5em 0.25em;
-}
-
-.alectryon-goal:target .goal-separator .alectryon-mref-marker,
-:target > .alectryon-mref-marker {
-    animation: blink 0.2s step-start 0s 3 normal none;
-    background-color: #fcaf3e;
-    position: relative;
-}
-
-@keyframes blink {
-    50% {
-        box-shadow: 0 0 0 3pt #fcaf3e, 0 0 0 4pt black;
-        z-index: 10;
-    }
-}
-
-.alectryon-toggle,
-.alectryon-io .alectryon-extra-goal-toggle {
-    display: none;
-}
-
-.alectryon-bubble,
-.alectryon-io label,
-.alectryon-toggle-label {
-    cursor: pointer;
-}
-
-.alectryon-toggle-label {
-    display: block;
-    font-size: 0.8em;
-}
-
-.alectryon-io .alectryon-input {
-    padding: 0.1em 0; /* Enlarge the hitbox slightly to fill interline gaps */
-}
-
-.alectryon-io .alectryon-token {
-    white-space: pre-wrap;
-    display: inline;
-}
-
-.alectryon-io .alectryon-sentence.alectryon-target .alectryon-input {
-    /* FIXME if keywords were ‘bolder’ we wouldn't need !important */
-    font-weight: bold !important; /* Use !important to avoid a * selector */
-}
-
-.alectryon-bubble:before,
-.alectryon-toggle-label:before,
-.alectryon-io label.alectryon-input:after,
-.alectryon-io .alectryon-goal > label:before {
-    border: 1px solid #babdb6;
-    border-radius: 1em;
-    box-sizing: border-box;
-    content: '';
-    display: inline-block;
-    font-weight: bold;
-    height: 0.25em;
-    margin-bottom: 0.15em;
-    vertical-align: middle;
-    width: 0.75em;
-}
-
-.alectryon-toggle-label:before,
-.alectryon-io .alectryon-goal > label:before {
-    margin-right: 0.25em;
-}
-
-.alectryon-io .alectryon-goal > label:before {
-    margin-top: 0.125em;
-}
-
-.alectryon-io label.alectryon-input {
-    padding-right: 1em; /* Prevent line wraps before the checkbox bubble */
-}
-
-.alectryon-io label.alectryon-input:after {
-    margin-left: 0.25em;
-    margin-right: -1em; /* Compensate for the anti-wrapping space */
-}
-
-.alectryon-failed {
-    /* Underlines are broken in Chrome (they reset at each element boundary)… */
-    /* text-decoration: red wavy underline; */
-    /* … but it isn't too noticeable with dots */
-    text-decoration: red dotted underline;
-    text-decoration-skip-ink: none;
-    /* Chrome prints background images in low resolution, yielding a blurry underline */
-    /* background: bottom / 0.3em auto repeat-x url(data:image/svg+xml;base64,PHN2ZyB4bWxucz0iaHR0cDovL3d3dy53My5vcmcvMjAwMC9zdmciIHZpZXdCb3g9IjAgMCAyLjY0NiAxLjg1MiIgaGVpZ2h0PSI4IiB3aWR0aD0iMTAiPjxwYXRoIGQ9Ik0wIC4yNjVjLjc5NCAwIC41MyAxLjMyMiAxLjMyMyAxLjMyMi43OTQgMCAuNTMtMS4zMjIgMS4zMjMtMS4zMjIiIGZpbGw9Im5vbmUiIHN0cm9rZT0icmVkIiBzdHJva2Utd2lkdGg9Ii41MjkiLz48L3N2Zz4=); */
-}
-
-/* Wrapping :hover rules in a media query ensures that tapping a Coq sentence
-   doesn't trigger its :hover state (otherwise, on mobile, tapping a sentence to
-   hide its output causes it to remain visible (its :hover state gets triggered.
-   We only do it for the default style though, since other styles don't put the
-   output over the main text, so showing too much is not an issue. */
-@media (any-hover: hover) {
-    .alectryon-bubble:hover:before,
-    .alectryon-toggle-label:hover:before,
-    .alectryon-io label.alectryon-input:hover:after {
-        background: #eeeeec;
-    }
-
-    .alectryon-io label.alectryon-input:hover {
-        text-decoration: underline dotted #babdb6;
-	    text-shadow: 0 0 1px rgb(46, 52, 54, 0.3); /* #2e3436 + opacity */
-    }
-
-    .alectryon-io .alectryon-sentence:hover .alectryon-output,
-    .alectryon-io .alectryon-token:hover .alectryon-type-info-wrapper,
-    .alectryon-io .alectryon-token:hover .alectryon-type-info-wrapper {
-        z-index: 2; /* Place hovered goals above .alectryon-sentence.alectryon-target ones */
-    }
-}
-
-.alectryon-toggle:checked + .alectryon-toggle-label:before,
-.alectryon-io .alectryon-sentence > .alectryon-toggle:checked + label.alectryon-input:after,
-.alectryon-io .alectryon-extra-goal-toggle:checked + .alectryon-goal > label:before {
-    background-color: #babdb6;
-    border-color: #babdb6;
-}
-
-/* Disable clicks on sentences when the document-wide toggle is set. */
-.alectryon-toggle:checked + label + .alectryon-container label.alectryon-input {
-    cursor: unset;
-    pointer-events: none;
-}
-
-/* Hide individual checkboxes when the document-wide toggle is set. */
-.alectryon-toggle:checked + label + .alectryon-container label.alectryon-input:after {
-    display: none;
-}
-
-/* .alectryon-output is displayed by toggles, :hover, and .alectryon-target rules */
-.alectryon-io .alectryon-output {
-    box-sizing: border-box;
-    display: none;
-    left: 0;
-    right: 0;
-    position: absolute;
-    padding: 0.25em 0;
-    overflow: visible; /* Let box-shadows overflow */
-    z-index: 1; /* Default to an index lower than that used by :hover */
-}
-
-.alectryon-io .alectryon-type-info-wrapper {
-    position: absolute;
-    display: inline-block;
-    width: 100%;
-}
-
-.alectryon-io .alectryon-type-info-wrapper.full-width {
-    left: 0;
-    min-width: 100%;
-    max-width: 100%;
-}
-
-.alectryon-io .alectryon-type-info .goal-separator {
-    height: unset;
-    margin-top: 0em;
-}
-
-.alectryon-io .alectryon-type-info-wrapper .alectryon-type-info {
-    box-sizing: border-box;
-    bottom: 100%;
-    position: absolute;
-    /*padding: 0.25em 0;*/
-    visibility: hidden;
-    overflow: visible; /* Let box-shadows overflow */
-    z-index: 1; /* Default to an index lower than that used by :hover */
-    white-space: pre-wrap !important;
-}
-
-.alectryon-io .alectryon-type-info-wrapper .alectryon-type-info .alectryon-goal.alectryon-docstring {
-    white-space: pre-wrap !important;
-}
-
-@media (any-hover: hover) { /* See note above about this @media query */
-    .alectryon-io .alectryon-sentence:hover .alectryon-output:not(:hover) {
-        display: block;
-    }
-
-    .alectryon-io.output-hidden .alectryon-sentence:hover .alectryon-output:not(:hover) {
-        display: none !important;
-    }
-
-    .alectryon-io.type-info-hidden .alectryon-token:hover .alectryon-type-info-wrapper .alectryon-type-info,
-    .alectryon-io.type-info-hidden .alectryon-token:hover .alectryon-type-info-wrapper .alectryon-type-info {
-        /*visibility: hidden !important;*/
-    }
-
-    .alectryon-io .alectryon-token:hover .alectryon-type-info-wrapper .alectryon-type-info,
-    .alectryon-io .alectryon-token:hover .alectryon-type-info-wrapper .alectryon-type-info {
-        visibility: visible;
-        transition-delay: 0.5s;
-    }
-}
-
-.alectryon-io .alectryon-sentence.alectryon-target .alectryon-output {
-    display: block;
-}
-
-/* Indicate active (hovered or targeted) goals with a shadow. */
-.alectryon-io .alectryon-sentence:hover .alectryon-output:not(:hover) .alectryon-messages,
-.alectryon-io .alectryon-sentence.alectryon-target .alectryon-output  .alectryon-messages,
-.alectryon-io .alectryon-sentence:hover .alectryon-output:not(:hover) .alectryon-goals,
-.alectryon-io .alectryon-sentence.alectryon-target .alectryon-output  .alectryon-goals,
-.alectryon-io .alectryon-token:hover .alectryon-type-info-wrapper .alectryon-type-info {
-    box-shadow: 2px 2px 2px gray;
-}
-
-.alectryon-io .alectryon-extra-goals .alectryon-goal .goal-hyps {
-    display: none;
-}
-
-.alectryon-io .alectryon-extra-goals .alectryon-extra-goal-toggle:not(:checked) + .alectryon-goal label.goal-separator hr {
-    /* Dashes indicate that the hypotheses are hidden */
-    border-top-style: dashed;
-}
-
-
-/* Show just a small preview of the other goals; this is undone by the
-   "extra-goal" toggle and by :hover and .alectryon-target in windowed mode. */
-.alectryon-io .alectryon-extra-goals .alectryon-goal .goal-conclusion {
-    max-height: 5.2em;
-    overflow-y: auto;
-    /* Combining ‘overflow-y: auto’ with ‘display: inline-block’ causes extra space
-       to be added below the box. ‘vertical-align: middle’ gets rid of it. */
-    vertical-align: middle;
-}
-
-.alectryon-io .alectryon-goals,
-.alectryon-io .alectryon-messages {
-    background: #f6f7f6;
-	/*border: thin solid #d3d7cf; /* Convenient when pre's background is already #EEE */
-    display: block;
-    padding: 0.25em;
-}
-
-.alectryon-message::before {
-    content: '';
-    float: right;
-    /* etc/svg/square-bubble-xl.svg */
-    background: url("data:image/svg+xml,%3Csvg width='14' height='14' viewBox='0 0 3.704 3.704' xmlns='http://www.w3.org/2000/svg'%3E%3Cg fill-rule='evenodd' stroke='%23000' stroke-width='.264'%3E%3Cpath d='M.794.934h2.115M.794 1.463h1.455M.794 1.992h1.852'/%3E%3C/g%3E%3Cpath d='M.132.14v2.646h.794v.661l.926-.661h1.72V.14z' fill='none' stroke='%23000' stroke-width='.265'/%3E%3C/svg%3E") top right no-repeat;
-    height: 14px;
-    width: 14px;
-}
-
-.alectryon-toggle:checked + label + .alectryon-container {
-    width: unset;
-}
-
-/* Show goals when a toggle is set */
-.alectryon-toggle:checked + label + .alectryon-container label.alectryon-input + .alectryon-output,
-.alectryon-io .alectryon-sentence > .alectryon-toggle:checked ~ .alectryon-output {
-    display: block;
-    position: static;
-    width: unset;
-    background: unset; /* Override the backgrounds set in floating in windowed mode */
-    padding: 0.25em 0; /* Re-assert so that later :hover rules don't override this padding */
-}
-
-.alectryon-toggle:checked + label + .alectryon-container label.alectryon-input + .alectryon-output .goal-hyps,
-.alectryon-io .alectryon-sentence > .alectryon-toggle:checked ~ .alectryon-output .goal-hyps {
-    /* Overridden back in windowed style */
-    flex-flow: row wrap;
-    justify-content: flex-start;
-}
-
-.alectryon-toggle:checked + label + .alectryon-container .alectryon-sentence .alectryon-output > div,
-.alectryon-io .alectryon-sentence > .alectryon-toggle:checked ~ .alectryon-output > div {
-    display: block;
-}
-
-.alectryon-io .alectryon-extra-goal-toggle:checked + .alectryon-goal .goal-hyps {
-    display: flex;
-}
-
-.alectryon-io .alectryon-extra-goal-toggle:checked + .alectryon-goal .goal-conclusion {
-    max-height: unset;
-    overflow-y: unset;
-}
-
-.alectryon-toggle:checked + label + .alectryon-container .alectryon-sentence > .alectryon-toggle ~ .alectryon-wsp,
-.alectryon-io .alectryon-sentence > .alectryon-toggle:checked ~ .alectryon-wsp {
-    display: none;
-}
-
-.alectryon-io .alectryon-messages,
-.alectryon-io .alectryon-message,
-.alectryon-io .alectryon-goals,
-.alectryon-io .alectryon-goal,
-.alectryon-io .goal-hyps > span,
-.alectryon-io .goal-conclusion {
-    border-radius: 0.15em;
-}
-
-.alectryon-io .alectryon-goal,
-.alectryon-io .alectryon-message {
-    align-items: center;
-    background: #f6f7f6;
-    border: 0em;
-    display: block;
-    flex-direction: column;
-    margin: 0.25em;
-    padding: 0.5em;
-    position: relative;
-}
-
-.alectryon-io .goal-hyps {
-    align-content: space-around;
-    align-items: baseline;
-    display: flex;
-    flex-flow: column nowrap; /* re-stated in windowed mode */
-    justify-content: space-around;
-    /* LATER use a ‘gap’ property instead of margins once supported */
-    margin: -0.15em -0.25em; /* -0.15em to cancel the item spacing */
-    padding-bottom: 0.35em; /* 0.5em-0.15em to cancel the 0.5em of .goal-separator */
-}
-
-.alectryon-io .goal-hyps > br {
-    display: none; /* Only for RSS readers */
-}
-
-.alectryon-io .goal-hyps > span,
-.alectryon-io .goal-conclusion {
-    /*background: #eeeeec;*/
-    display: inline-block;
-    padding: 0.15em 0.35em;
-}
-
-.alectryon-io .goal-hyps > span {
-    align-items: baseline;
-    display: inline-flex;
-    margin: 0.15em 0.25em;
-}
-
-.alectryon-block var,
-.alectryon-inline var,
-.alectryon-io .goal-hyps > span > var {
-    font-weight: 600;
-    font-style: unset;
-}
-
-.alectryon-io .goal-hyps > span > var {
-    /* Shrink the list of names, but let it grow as long as space is available. */
-    flex-basis: min-content;
-    flex-grow: 1;
-}
-
-.alectryon-io .goal-hyps > span b {
-    font-weight: 600;
-    margin: 0 0 0 0.5em;
-    white-space: pre;
-}
-
-.alectryon-io .hyp-body,
-.alectryon-io .hyp-type {
-    display: flex;
-    align-items: baseline;
-}
-
-.alectryon-io .goal-separator {
-    align-items: center;
-    display: flex;
-    flex-direction: row;
-    height: 1em; /* Fixed height to ignore goal name and markers */
-    margin-top: -0.5em; /* Compensated in .goal-hyps when shown */
-}
-
-.alectryon-io .goal-separator hr {
-    border: none;
-    border-top: thin solid #555753;
-    display: block;
-    flex-grow: 1;
-    margin: 0;
-}
-
-.alectryon-io .goal-separator .goal-name {
-    font-size: 0.75em;
-    margin-left: 0.5em;
-}
-
-/**********/
-/* Banner */
-/**********/
-
-.alectryon-banner {
-    background: #eeeeec;
-    border: 1px solid #babcbd;
-    font-size: 0.75em;
-    padding: 0.25em;
-    text-align: center;
-    margin: 1em 0;
-}
-
-.alectryon-banner a {
-    cursor: pointer;
-    text-decoration: underline;
-}
-
-.alectryon-banner kbd {
-    background: #d3d7cf;
-    border-radius: 0.15em;
-    border: 1px solid #babdb6;
-    box-sizing: border-box;
-    display: inline-block;
-    font-family: inherit;
-    font-size: 0.9em;
-    height: 1.3em;
-    line-height: 1.2em;
-    margin: -0.25em 0;
-    padding: 0 0.25em;
-    vertical-align: middle;
-}
-
-/**********/
-/* Toggle */
-/**********/
-
-.alectryon-toggle-label {
-    margin: 1rem 0;
-}
-
-/******************/
-/* Floating style */
-/******************/
-
-/* If there's space, display goals to the right of the code, not below it. */
-@media (min-width: 80rem) {
-    /* Unlike the windowed case, we don't want to move output blocks to the side
-       when they are both :checked and -targeted, since it gets confusing as
-       things jump around; hence the commented-output part of the selector,
-       which would otherwise increase specificity */
-    .alectryon-floating .alectryon-sentence.alectryon-target /* > .alectryon-toggle ~ */ .alectryon-output,
-    .alectryon-floating .alectryon-sentence:hover .alectryon-output {
-        top: 0;
-        left: 100%;
-        right: -100%;
-        padding: 0 0.5em;
-        position:  absolute;
-    }
-
-    .alectryon-floating .alectryon-output {
-        min-height: 100%;
-    }
-
-    .alectryon-floating .alectryon-sentence:hover .alectryon-output {
-        background: white; /* Ensure that short goals hide long ones */
-    }
-
-    /* This odd margin-bottom property prevents the sticky div from bumping
-       against the bottom of its container (.alectryon-output).  The alternative
-       would be enlarging .alectryon-output, but that would cause overflows,
-       enlarging scrollbars and yielding scrolling towards the bottom of the
-       page.  Doing things this way instead makes it possible to restrict
-       .alectryon-output to a reasonable size (100%, through top = bottom = 0).
-       See also https://stackoverflow.com/questions/43909940/. */
-    /* See note on specificity above */
-    .alectryon-floating .alectryon-sentence.alectryon-target /* > .alectryon-toggle ~ */ .alectryon-output > div,
-    .alectryon-floating .alectryon-sentence:hover .alectryon-output > div {
-        margin-bottom: -200%;
-        position: sticky;
-        top: 0;
-    }
-
-    .alectryon-floating .alectryon-toggle:checked + label + .alectryon-container .alectryon-sentence .alectryon-output > div,
-    .alectryon-floating .alectryon-io .alectryon-sentence > .alectryon-toggle:checked ~ .alectryon-output > div {
-        margin-bottom: unset; /* Undo the margin */
-    }
-
-    /* Float underneath the current fragment
-    @media (max-width: 80rem) {
-        .alectryon-floating .alectryon-output {
-            top: 100%;
-        }
-    } */
-}
-
-/********************/
-/* Multi-pane style */
-/********************/
-
-.alectryon-windowed {
-    border: 0 solid #2e3436;
-    box-sizing: border-box;
-}
-
-.alectryon-windowed .alectryon-sentence:hover .alectryon-output {
-    background: white; /* Ensure that short goals hide long ones */
-}
-
-.alectryon-windowed .alectryon-output {
-    position: fixed; /* Overwritten by the ‘:checked’ rules */
-}
-
-/* See note about specificity below */
-.alectryon-windowed .alectryon-sentence:hover .alectryon-output,
-.alectryon-windowed .alectryon-sentence.alectryon-target > .alectryon-toggle ~ .alectryon-output {
-    padding: 0.5em;
-    overflow-y: auto; /* Windowed contents may need to scroll */
-}
-
-.alectryon-windowed .alectryon-io .alectryon-sentence:hover .alectryon-output:not(:hover) .alectryon-messages,
-.alectryon-windowed .alectryon-io .alectryon-sentence.alectryon-target .alectryon-output  .alectryon-messages,
-.alectryon-windowed .alectryon-io .alectryon-sentence:hover .alectryon-output:not(:hover) .alectryon-goals,
-.alectryon-windowed .alectryon-io .alectryon-sentence.alectryon-target .alectryon-output  .alectryon-goals {
-    box-shadow: none; /* A shadow is unnecessary here and incompatible with overflow-y set to auto */
-}
-
-.alectryon-windowed .alectryon-io .alectryon-sentence.alectryon-target .alectryon-output .goal-hyps {
-    /* Restated to override the :checked style */
-    flex-flow: column nowrap;
-    justify-content: space-around;
-}
-
-
-.alectryon-windowed .alectryon-sentence.alectryon-target .alectryon-extra-goals .alectryon-goal .goal-conclusion
-/* Like .alectryon-io .alectryon-extra-goal-toggle:checked + .alectryon-goal .goal-conclusion */ {
-    max-height: unset;
-    overflow-y: unset;
-}
-
-.alectryon-windowed .alectryon-output > div {
-    display: flex; /* Put messages after goals */
-    flex-direction: column-reverse;
-}
-
-/*********************/
-/* Standalone styles */
-/*********************/
-
-.alectryon-standalone {
-    font-family: 'IBM Plex Serif', 'PT Serif', 'Merriweather', 'DejaVu Serif', serif;
-    line-height: 1.5;
-}
-
-@media screen and (min-width: 50rem) {
-    html.alectryon-standalone {
-        /* Prevent flickering when hovering a block causes scrollbars to appear. */
-        margin-left: calc(100vw - 100%);
-        margin-right: 0;
-    }
-}
-
-/* Coqdoc */
-
-.alectryon-coqdoc .doc .code,
-.alectryon-coqdoc .doc .inlinecode,
-.alectryon-coqdoc .doc .comment {
-    display: inline;
-}
-
-.alectryon-coqdoc .doc .comment {
-    color: #eeeeec;
-}
-
-.alectryon-coqdoc .doc .paragraph {
-    height: 0.75em;
-}
-
-/* Centered, Floating */
-
-.alectryon-standalone .alectryon-centered,
-.alectryon-standalone .alectryon-floating {
-    max-width: 50rem;
-    margin: auto;
-}
-
-@media (min-width: 80rem) {
-    .alectryon-standalone .alectryon-floating {
-        max-width: 80rem;
-    }
-
-    .alectryon-standalone .alectryon-floating > * {
-        width: 50%;
-        margin-left: 0;
-    }
-}
-
-/* Windowed */
-
-.alectryon-standalone .alectryon-windowed {
-    display: block;
-    margin: 0;
-    overflow-y: auto;
-    position: absolute;
-    padding: 0 1em;
-}
-
-.alectryon-standalone .alectryon-windowed > * {
-    /* Override properties of docutils_basic.css */
-    margin-left: 0;
-    max-width: unset;
-}
-
-.alectryon-standalone .alectryon-windowed .alectryon-io {
-    box-sizing: border-box;
-    width: 100%;
-}
-
-/* No need to predicate the ‘:hover’ rules below on ‘:not(:checked)’, since ‘left’,
-   ‘right’, ‘top’, and ‘bottom’ will be inactived by the :checked rules setting
-   ‘position’ to ‘static’ */
-
-
-/* Specificity: We want the output to stay inline when hovered while unfolded
-   (:checked), but we want it to move when it's targeted (i.e. when the user
-   is browsing goals one by one using the keyboard, in which case we want to
-   goals to appear in consistent locations).  The selectors below ensure
-   that :hover < :checked < -targeted in terms of specificity. */
-/* LATER: Reimplement this stuff with CSS variables */
-.alectryon-windowed .alectryon-sentence.alectryon-target > .alectryon-toggle ~ .alectryon-output {
-    position: fixed;
-}
-
-@media screen and (min-width: 60rem) {
-    .alectryon-standalone .alectryon-windowed {
-        border-right-width: thin;
-        bottom: 0;
-        left: 0;
-        right: 50%;
-        top: 0;
-    }
-
-    .alectryon-standalone .alectryon-windowed .alectryon-sentence:hover .alectryon-output,
-    .alectryon-standalone .alectryon-windowed .alectryon-sentence.alectryon-target .alectryon-output {
-        bottom: 0;
-        left: 50%;
-        right: 0;
-        top: 0;
-    }
-}
-
-@media screen and (max-width: 60rem) {
-    .alectryon-standalone .alectryon-windowed {
-        border-bottom-width: 1px;
-        bottom: 40%;
-        left: 0;
-        right: 0;
-        top: 0;
-    }
-
-    .alectryon-standalone .alectryon-windowed .alectryon-sentence:hover .alectryon-output,
-    .alectryon-standalone .alectryon-windowed .alectryon-sentence.alectryon-target .alectryon-output {
-        bottom: 0;
-        left: 0;
-        right: 0;
-        top: 60%;
-    }
-}

doc/alectryon.js

@@ -1,190 +0,0 @@
-var Alectryon;
-(function(Alectryon) {
-    (function (slideshow) {
-        function anchor(sentence) { return "#" + sentence.id; }
-
-        function current_sentence() { return slideshow.sentences[slideshow.pos]; }
-
-        function unhighlight() {
-            var sentence = current_sentence();
-            if (sentence) sentence.classList.remove("alectryon-target");
-            slideshow.pos = -1;
-        }
-
-        function highlight(sentence) {
-            sentence.classList.add("alectryon-target");
-        }
-
-        function scroll(sentence) {
-            // Put the top of the current fragment close to the top of the
-            // screen, but scroll it out of view if showing it requires pushing
-            // the sentence past half of the screen.  If sentence is already in
-            // a reasonable position, don't move.
-            var parent = sentence.parentElement;
-            /* We want to scroll the whole document, so start at root… */
-            while (parent && !parent.classList.contains("alectryon-root"))
-                parent = parent.parentElement;
-            /* … and work up from there to find a scrollable element.
-               parent.scrollHeight can be greater than parent.clientHeight
-               without showing scrollbars, so we add a 10px buffer. */
-            while (parent && parent.scrollHeight <= parent.clientHeight + 10)
-                parent = parent.parentElement;
-            /* <body> and <html> elements can have their client rect overflow
-             * the window if their height is unset, so scroll the window
-             * instead */
-            if (parent && (parent.nodeName == "BODY" || parent.nodeName == "HTML"))
-                parent = null;
-
-            var rect = function(e) { return e.getBoundingClientRect(); };
-            var parent_box = parent ? rect(parent) : { y: 0, height: window.innerHeight },
-                sentence_y = rect(sentence).y - parent_box.y,
-                fragment_y = rect(sentence.parentElement).y - parent_box.y;
-
-            // The assertion below sometimes fails for the first element in a block.
-            // console.assert(sentence_y >= fragment_y);
-
-            if (sentence_y < 0.1 * parent_box.height ||
-                sentence_y > 0.7 * parent_box.height) {
-                (parent || window).scrollBy(
-                    0, Math.max(sentence_y - 0.5 * parent_box.height,
-                                fragment_y - 0.1 * parent_box.height));
-            }
-        }
-
-        function highlighted(pos) {
-            return slideshow.pos == pos;
-        }
-
-        function navigate(pos, inhibitScroll) {
-            unhighlight();
-            slideshow.pos = Math.min(Math.max(pos, 0), slideshow.sentences.length - 1);
-            var sentence = current_sentence();
-            highlight(sentence);
-            if (!inhibitScroll)
-                scroll(sentence);
-        }
-
-        var keys = {
-            PAGE_UP: 33,
-            PAGE_DOWN: 34,
-            ARROW_UP: 38,
-            ARROW_DOWN: 40,
-            h: 72, l: 76, p: 80, n: 78
-        };
-
-        function onkeydown(e) {
-            e = e || window.event;
-            if (e.ctrlKey || e.metaKey) {
-                if (e.keyCode == keys.ARROW_UP)
-                    slideshow.previous();
-                else if (e.keyCode == keys.ARROW_DOWN)
-                    slideshow.next();
-                else
-                    return;
-            } else {
-                // if (e.keyCode == keys.PAGE_UP || e.keyCode == keys.p || e.keyCode == keys.h)
-                //     slideshow.previous();
-                // else if (e.keyCode == keys.PAGE_DOWN || e.keyCode == keys.n || e.keyCode == keys.l)
-                //     slideshow.next();
-                // else
-                return;
-            }
-            e.preventDefault();
-        }
-
-        function start() {
-            slideshow.navigate(0);
-        }
-
-        function toggleHighlight(idx) {
-            if (highlighted(idx))
-                unhighlight();
-            else
-                navigate(idx, true);
-        }
-
-        function handleClick(evt) {
-            if (evt.ctrlKey || evt.metaKey) {
-                var sentence = evt.currentTarget;
-
-                // Ensure that the goal is shown on the side, not inline
-                var checkbox = sentence.getElementsByClassName("alectryon-toggle")[0];
-                if (checkbox)
-                    checkbox.checked = false;
-
-                toggleHighlight(sentence.alectryon_index);
-                evt.preventDefault();
-            }
-        }
-
-        function init() {
-            document.onkeydown = onkeydown;
-            slideshow.pos = -1;
-            slideshow.sentences = Array.from(document.getElementsByClassName("alectryon-sentence"));
-            slideshow.sentences.forEach(function (s, idx) {
-                s.addEventListener('click', handleClick, false);
-                s.alectryon_index = idx;
-            });
-        }
-
-        slideshow.start = start;
-        slideshow.end = unhighlight;
-        slideshow.navigate = navigate;
-        slideshow.next = function() { navigate(slideshow.pos + 1); };
-        slideshow.previous = function() { navigate(slideshow.pos + -1); };
-        window.addEventListener('DOMContentLoaded', init);
-    })(Alectryon.slideshow || (Alectryon.slideshow = {}));
-
-    (function (styles) {
-        var styleNames = ["centered", "floating", "windowed"];
-
-        function className(style) {
-            return "alectryon-" + style;
-        }
-
-        function setStyle(style) {
-            var root = document.getElementsByClassName("alectryon-root")[0];
-            styleNames.forEach(function (s) {
-                root.classList.remove(className(s)); });
-            root.classList.add(className(style));
-        }
-
-        function init() {
-            var banner = document.getElementsByClassName("alectryon-banner")[0];
-            if (banner) {
-                banner.append(" Style: ");
-                styleNames.forEach(function (styleName, idx) {
-                    var s = styleName;
-                    var a = document.createElement("a");
-                    a.onclick = function() { setStyle(s); };
-                    a.append(styleName);
-                    if (idx > 0) banner.append("; ");
-                    banner.appendChild(a);
-                });
-                banner.append(".");
-            }
-        }
-
-        window.addEventListener('DOMContentLoaded', init);
-
-        styles.setStyle = setStyle;
-    })(Alectryon.styles || (Alectryon.styles = {}));
-})(Alectryon || (Alectryon = {}));
-
-function setHidden(elements, isVisible, token) {
-    for (let i = 0; i < elements.length; i++) {
-        if (isVisible) {
-            elements[i].classList.remove(token)
-        } else {
-            elements[i].classList.add(token)
-        }
-    }
-}
-
-function toggleShowTypes(checkbox) {
-    setHidden(document.getElementsByClassName("alectryon-io"), checkbox.checked, "type-info-hidden")
-}
-
-function toggleShowGoals(checkbox) {
-    setHidden(document.getElementsByClassName("alectryon-io"), checkbox.checked, "output-hidden")
-}

doc/array.md

@@ -39,17 +39,16 @@ To create an array of size `n` in which all the elements are initialized to some
 
 You can access array elements by using brackets (`[` and `]`).
 ```lean
-def f (a : Array Nat) (i : Fin a.size) :=
-  a[i] + a[i]
-```
-Note that the index `i` has type `Fin a.size`, i.e., it is natural number less than `a.size`.
-You can also write
-```lean
-def f (a : Array Nat) (i : Nat) (h  : i < a.size) :=
-  a[i] + a[i]
+#eval #['a', 'b', 'c'][1]
+-- 'b'
+
+def getThird (xs : Array Nat) : Nat :=
+  xs[2]
+
+#eval getThird #[10, 20, 30, 40]
+-- 30
 ```
 The bracket operator is whitespace sensitive.
-
 ```lean
 def f (xs : List Nat) : List Nat :=
   xs ++ xs
@@ -57,21 +56,7 @@ def f (xs : List Nat) : List Nat :=
 def as : Array Nat :=
   #[1, 2, 3, 4]
 
-def idx : Fin 4 :=
-  2
-
 #eval f [1, 2, 3] -- This is a function application
 
-#eval as[idx] -- This is an array access
-```
-The notation `a[i]` has two variants: `a[i]!` and `a[i]?`. In both cases, `i` has type `Nat`. The first one
-produces a panic error message if the index `i` is out of bounds. The latter returns an `Option` type.
-
-```lean
-#eval #['a', 'b', 'c'][1]?
--- some 'b'
-#eval #['a', 'b', 'c'][5]?
--- none
-#eval #['a', 'b', 'c'][1]!
--- 'b!
+#eval as[2] -- This is an array access
 ```

doc/autobound.md

@@ -36,12 +36,10 @@ Note that, Lean inferred a more general type using `Sort` instead of `Type`.
 
 Although we love this feature and use it extensively when implementing Lean,
 we realize some users may feel uncomfortable with it. Thus, you can disable it using
-the command `set_option autoImplicit false`.
+the command `set_option autoBoundImplicitLocal false`.
 ```lean
-set_option autoImplicit false
+set_option autoBoundImplicitLocal false
 /- The following definition produces `unknown identifier` errors -/
 -- def compose (g : β → γ) (f : α → β) (x : α) : γ :=
 --   g (f x)
 ```
-The Lean language server provides [semantic highlighting](./semantic_highlighting.md) information to editors, and it provides
-visual feedback whether an identifier has been interpreted as an auto bound implicit argument.

doc/book.toml

@@ -10,12 +10,6 @@ build-dir = "out"
 
 [output.html]
 git-repository-url = "https://github.com/leanprover/lean4"
-additional-css = ["alectryon.css", "pygments.css"]
-additional-js = ["alectryon.js"]
-
-[output.html.fold]
-enable = true
-level = 0
 
 [output.html.playground.boring-prefixes]
 lean = "# "

doc/bool.md

@@ -1 +0,0 @@
-# Booleans

doc/coding_style.md

@@ -0,0 +1,244 @@
+Coding Style
+============
+
+[C++11](http://en.wikipedia.org/wiki/C%2B%2B11) features
+--------------------------------------------------------
+
+We make extensive use of new features in the C++ 11 standard.
+Developers must be familiar with the standard to be able to understand
+the code.
+Here are some of the features that are extensively used.
+
+- Type inference (aka `auto` keyword).
+- Initializer lists.
+- Lambda functions and expressions.
+- `nullptr` constant.
+- Strongly typed enumerations.
+- Right angle bracket.
+- Thread local storage.
+- Threading facilities.
+- Tuple types.
+
+Comments
+--------
+
+The comments in the Lean codebase contain
+[Doxygen](http://www.stack.nl/~dimitri/doxygen/) commands.
+Doxygen is the de facto standard tool for generating documentation from
+annotated C++ sources.
+
+Namespaces
+----------
+
+All code is in the `lean` namespace. Each frontend is stored in a
+separate nested namespace. For example, the SMT 2.0 frontend is stored
+in the `lean::smt` namespace.
+
+Exception: some debugging functions are stored outside of the `lean`
+namespace. These functions are called `print` and are meant to be used
+when debugging Lean using `gdb`.
+
+Smart pointers
+--------------
+
+We only use `std::shared_ptr` template for class `C` only if we expect
+to create only a few objects (< 1000) of class `C`. Otherwise, we
+implement our own intrusive smart pointer. For example, the class
+`expr` is an intrusive smart pointer to `expr_cell`. We may have
+millions of `expr` objects. We say it is intrusive because the
+reference counter is stored in `expr_cell`.
+
+We use `std::unique_ptr` to make sure unique resources will be freed
+correctly.
+
+Template
+--------
+We organize template source code using the approach described at http://www.codeproject.com/Articles/3515/How-To-Organize-Template-Source-Code
+
+Idioms
+------
+
+We use some popular C++ idioms:
+
+- [Pimpl](http://c2.com/cgi/wiki?PimplIdiom)
+- [RAII](http://en.wikipedia.org/wiki/Resource_Acquisition_Is_Initialization) Resource Acquisition Is Initialization
+
+Formatting
+----------
+
+* We use 4 spaces for indentation.
+
+* Class, method, and function names are lower case
+We use `_` for composite names. Example: `type_checker`.
+
+* Class/struct fields should start with the prefix `m_`.
+
+Example:
+
+     class point {
+         int m_x;
+         int m_y;
+     public:
+         ...
+     };
+
+* We do **not** use the `#ifndef-#define-#endif` idiom for header files.
+Instead we use `#pragma once`.
+
+* We write `type const & v` instead of `const type & v`.
+
+* We use `const` extensively.
+
+* `if-then-else`
+
+The following forms are acceptable:
+
+     if (cond) {
+         ...
+     } else {
+         ...
+     }
+
+and
+
+     if (cond)
+        statement1;
+     else
+        statement2;
+
+In *exceptional cases*, we also use
+
+     if (cond) statement;
+
+and
+
+     if (cond) statement1; else stament2;
+
+* `if-then-else-if-else`
+
+The following forms are acceptable:
+
+     if (cond) {
+         ...
+     } else if (cond) {
+         ...
+     } else {
+         ...
+     }
+
+and
+
+     if (cond)
+         statement1;
+     else if (cond)
+         statement2;
+     else
+         statement3;
+
+* We frequently format code using extra spaces
+
+For example, we write
+
+    environment const & m_env;
+    cache               m_cache;
+    normalizer          m_normalizer;
+    volatile bool       m_interrupted;
+
+instead of
+
+    environment const & m_env;
+    cache m_cache;
+    normalizer m_normalizer;
+    volatile bool m_interrupted;
+
+* We use the macro `lean_assert` for assertions.
+The macro `lean_assert` is extensively used when writing unit tests.
+
+* Spaces in expressions
+We write `a == b` instead of `a==b`.
+Similarly, we write `x < y + 1` instead of `x<y+1`.
+
+Google's C++ Style Guide
+------------------------
+
+We are using a modified version of [Google's C++ Style Guide][google-style].
+We also have our version of Google's style checker [cpplint.py][cpplint].
+You can run the checker over the codebase by typing:
+
+    make style
+
+If you use Ninja, you can check by ``ninja style``. It is also a part of testcases and can be run by
+
+    ctest -R style_check
+
+*Disabled* Features:
+
+ - Namespace should be terminated with "namespace"
+ - At least two spaces is best between code and comments
+ - Do not use ``dynamic_cast<>``.  If you need to cast within a class
+   hierarchy, use ``static_cast<>`` to upcast.  Google doesn't support
+   RTTI.
+ - "public:" should be preceded by a blank line
+ - Missing space before ``{``
+ - Found C system header after C++ system header. Should be:
+   environment.h, c system, c++ system, other.
+ - Labels should always be indented at least one space.  If this is
+   a member-initializer list in a constructor or the base class list in
+   a class definition, the colon should be on the following line.
+ - You don't need a ``;`` after a ``}``
+ - No ``#ifndef`` header guard found
+ - Streams are highly discouraged.
+ - Extra space before ``(`` in function call
+ - Else clause should never be on same line as else
+ - Extra space before ``)``
+ - Is this a non-const reference? If so, make const or use a pointer.
+ - All parameters should be named in a function
+ - Do not use anonymous constructor notation (e.g., ``{a1, ..., an}``)
+
+Modified Features:
+
+  - Add ``#include <list>`` for ``list<>``
+
+    => *Check* ``std::list`` instead of ``list`` because we do have our own ``lean::list`` type.
+
+  - Add ``#include <algorithm>`` for copy
+
+    => *Check* ``std::copy`` instead of ``copy`` because we do have our own ``lean::copy`` method.
+
+  - Do not use namespace using-directives. Use using-declarations instead.
+
+    => *Allow* this if filename contains "tests/"
+
+  - Small and focused functions are preferred: foo()
+    has xxx non-comment lines (error triggered by exceeding 500 lines).
+
+    => *Allow* this if filename contains "tests/"
+
+  - Include the directory when naming .h files
+
+    => *Allow* this if the included filename is "version.h" which is generated by cmake.
+
+[google-style]: http://google-styleguide.googlecode.com/svn/trunk/cppguide.xml
+[cpplint]: /src/cmake/Modules/cpplint.py
+
+Git pre-push hook
+-----------------
+
+Since [git 1.8.2][git-pre-push-hook], git introduced *pre-push* hook
+which is executed *before* actual push operation is performed. Using this,
+we can *automatically* run the style checker over the changed files *before*
+we push commits to repositories. This is useful because it prevents us
+from accidentally pushing the commits which contain style problems.
+
+[git-pre-push-hook]: https://github.com/git/git/blob/master/Documentation/RelNotes/1.8.2.txt
+
+To activate the hook, execute
+
+```bash
+ln -s ../../script/pre-push .git/hooks
+```
+
+in the project root directory.
+
+You can change the ``CHECKER`` variable in the script if you want to use other
+checkers.

doc/debugging.md

@@ -20,9 +20,8 @@ Notable trace classes:
 * `Meta.isDefEq`: unification
 * `interpreter`: full execution trace of the interpreter. Only available in debug builds.
 
-In pure contexts or when execution is aborted before the messages are finally printed, one can instead use the term `dbg_trace "msg with {interpolations}"; val` (`;` can also be replaced by a newline), which will print the message to stderr before evaluating `val`. `dbgTraceVal val` can be used as a shorthand for `dbg_trace "{val}"; val`.
+In pure contexts or when execution is aborted before the messages are finally printed, one can instead use the term `dbg_trace "msg with {interpolations}"; val` (`;` can also be replaced by a newline), which will print the message directly to stderr before evaluating `val`. `dbgTraceVal val` can be used as a shorthand for `dbg_trace "{val}"; val`.
 Note that if the return value is not actually used, the trace code is silently dropped as well.
-In the language server, stderr output is buffered and shown as messages after a command has been elaborated, unless the option `server.stderrAsMessages` is deactivated.
 
 ## Debuggers
 

doc/declarations.md

@@ -1,797 +0,0 @@
-# Declarations
-
--- TODO (fix)
-
-Declaration Names
-=================
-
-A declaration name is a hierarchical [identifier](lexical_structure.md#identifiers) that is interpreted relative to the current namespace as well as (during lookup) to the set of open namespaces.
-
-```lean
-namespace A
-  opaque B.c : Nat
-  #print B.c -- opaque A.B.c : Nat
-end A
-
-#print A.B.c -- opaque A.B.c : Nat
-open A
-#print B.c -- opaque A.B.c : Nat
-```
-
-Declaration names starting with an underscore are reserved for internal use. Names starting with the special atomic name ``_root_`` are interpreted as absolute names.
-
-```lean
-opaque a : Nat
-namespace A
-  opaque a : Int
-  #print _root_.a -- opaque a : Nat
-  #print A.a      -- opaque A.a : Int
-end A
-```
-
-Contexts and Telescopes
-=======================
-
-When processing user input, Lean first parses text to a raw expression format. It then uses background information and type constants to disambiguate overloaded symbols and infer implicit arguments, resulting in a fully-formed expression. This process is known as *elaboration*.
-
-As hinted in [Expression Syntax](expressions.md#expression_syntax),
-expressions are parsed and elaborated with respect to an *environment*
-and a *local context*. Roughly speaking, an environment represents the
-state of Lean at the point where an expression is parsed, including
-previously declared axioms, constants, definitions, and theorems. In a
-given environment, a *local context* consists of a sequence ``(a₁ :
-α₁) (a₂ : α₂) ... (aₙ : αₙ)`` where each ``aᵢ`` is a name denoting a
-local constant and each ``αᵢ`` is an expression of type ``Sort u`` for
-some ``u`` which can involve elements of the environment and the local
-constants ``aⱼ`` for ``j < i``.
-
-Intuitively, a local context is a list of variables that are held constant while an expression is being elaborated. Consider the following
-
-```lean
-def f (a b : Nat) : Nat → Nat := fun c => a + (b + c)
-```
-
-Here the expression ``fun c => a + (b + c)`` is elaborated in the context ``(a : Nat) (b : Nat)`` and the expression ``a + (b + c)`` is elaborated in the context ``(a : Nat) (b : Nat) (c : Nat)``. If you replace the expression ``a + (b + c)`` with an underscore, the error message from Lean will include the current *goal*:
-
-```
-a b c : Nat
-⊢ Nat
-```
-
-Here ``a b c : Nat`` indicates the local context, and the second ``Nat`` indicates the expected type of the result.
-
-A *context* is sometimes called a *telescope*, but the latter is used more generally to include a sequence of declarations occurring relative to a given context. For example, relative to the context ``(a₁ : α₁) (a₂ : α₂) ... (aₙ : αₙ)``, the types ``βᵢ`` in a telescope ``(b₁ : β₁) (b₂ : β₂) ... (bₙ : βₙ)`` can refer to ``a₁, ..., aₙ``. Thus a context can be viewed as a telescope relative to the empty context.
-
-Telescopes are often used to describe a list of arguments, or parameters, to a declaration. In such cases, it is often notationally convenient to let ``(a : α)`` stand for a telescope rather than just a single argument. In general, the annotations described in [Implicit Arguments](expressions.md#implicit_arguments) can be used to mark arguments as implicit.
-
-.. _basic_declarations:
-
-Basic Declarations
-==================
-
-Lean provides ways of adding new objects to the environment. The following provide straightforward ways of declaring new objects:
-
-* ``axiom c : α`` :  declare a constant named ``c`` of type ``α``, it is postulating that `α` is not an empty type.
-* ``def c : α := v`` : defines ``c`` to denote ``v``, which should have type ``α``.
-* ``theorem c : p := v`` : similar to ``def``, but intended to be used when ``p`` is a proposition.
-* ``opaque c : α (:= v)?`` : declares a opaque constant named ``c`` of type ``α``, the optional value `v` is must have type `α`
-  and can be viewed as a certificate that ``α`` is not an empty type. If the value is not provided, Lean tries to find one
-  using a procedure based on type class resolution. The value `v` is hidden from the type checker. You can assume that
-  Lean "forgets" `v` after type checking this kind of declaration.
-
-It is sometimes useful to be able to simulate a definition or theorem without naming it or adding it to the environment.
-
-* ``example : α := t`` : elaborates ``t`` and checks that it has sort ``α`` (often a proposition), without adding it to the environment.
-
-In ``def``, the type (``α`` or ``p``, respectively) can be omitted when it can be inferred by Lean. Constants declared with ``theorem`` are marked as ``irreducible``.
-
-Any of ``def``, ``theorem``, ``axiom``, or ``example`` can take a list of arguments (that is, a context) before the colon. If ``(a : α)`` is a context, the definition ``def foo (a : α) : β := t``
-is interpreted as ``def foo : (a : α) → β := fun a : α => t``. Similarly, a theorem ``theorem foo (a : α) : p := t`` is interpreted as ``theorem foo : ∀ a : α, p := fun a : α => t``.
-
-```lean
-opaque c : Nat
-opaque d : Nat
-axiom cd_eq : c = d
-
-def foo : Nat := 5
-def bar := 6
-def baz (x y : Nat) (s : List Nat) := [x, y] ++ s
-
-theorem foo_eq_five : foo = 5 := rfl
-theorem baz_theorem (x y : Nat) : baz x y [] = [x, y] := rfl
-
-example (x y : Nat) : baz x y [] = [x, y] := rfl
-```
-
-Inductive Types
-===============
-
-Lean's axiomatic foundation allows users to declare arbitrary
-inductive families, following the pattern described by [Dybjer]_. To
-make the presentation more manageable, we first describe inductive
-*types*, and then describe the generalization to inductive *families*
-in the next section. The declaration of an inductive type has the
-following form:
-
-```
-inductive Foo (a : α) where
-  | constructor₁ : (b : β₁) → Foo a
-  | constructor₂ : (b : β₂) → Foo a
-  ...
-  | constructorₙ : (b : βₙ) → Foo a
-```
-
-Here ``(a : α)`` is a context and each ``(b : βᵢ)`` is a telescope in the context ``(a : α)`` together with ``Foo``, subject to the following constraints.
-
-Suppose the telescope ``(b : βᵢ)`` is ``(b₁ : βᵢ₁) ... (bᵤ : βᵢᵤ)``. Each argument in the telescope is either *nonrecursive* or *recursive*.
-
-- An argument ``(bⱼ : βᵢⱼ)`` is *nonrecursive* if ``βᵢⱼ`` does not refer to ``foo,`` the inductive type being defined. In that case, ``βᵢⱼ`` can be any type, so long as it does not refer to any nonrecursive arguments.
-
-- An argument ``(bⱼ : βᵢⱼ)`` is *recursive* if it ``βᵢⱼ`` of the form ``Π (d : δ), foo`` where ``(d : δ)`` is a telescope which does not refer to ``foo`` or any nonrecursive arguments.
-
-The inductive type ``foo`` represents a type that is freely generated by the constructors. Each constructor can take arbitrary data and facts as arguments (the nonrecursive arguments), as well as indexed sequences of elements of ``foo`` that have been previously constructed (the recursive arguments). In set theoretic models, such sets can be represented by well-founded trees labeled by the constructor data, or they can defined using other transfinite or impredicative means.
-
-The declaration of the type ``foo`` as above results in the addition of the following constants to the environment:
-
-- the *type former* ``foo : Π (a : α), Sort u``
-- for each ``i``, the *constructor* ``foo.constructorᵢ : Π (a : α) (b : βᵢ), foo a``
-- the *eliminator* ``foo.rec``, which takes arguments
-
-  + ``(a : α)`` (the parameters)
-  + ``{C : foo a → Type u}`` (the *motive* of the elimination)
-  + for each ``i``, the *minor premise* corresponding to ``constructorᵢ``
-  + ``(x : foo)`` (the *major premise*)
-
-  and returns an element of ``C x``. Here, The ith minor premise is a function which takes
-
-  +  ``(b : βᵢ)`` (the arguments to the constructor)
-  + an argument of type ``Π (d : δ), C (bⱼ d)`` corresponding to each recursive argument ``(bⱼ : βᵢⱼ)``, where ``βᵢⱼ``  is of the form ``Π (d : δ), foo`` (the recursive values of the function being defined)
-
-  and returns an element of ``C (constructorᵢ a b)``, the intended value of the function at ``constructorᵢ a b``.
-
-The eliminator represents a principle of recursion: to construct an element of ``C x`` where ``x : foo a``, it suffices to consider each of the cases where ``x`` is of the form ``constructorᵢ a b`` and to provide an auxiliary construction in each case. In the case where some of the arguments to ``constructorᵢ`` are recursive, we can assume that we have already constructed values of ``C y`` for each value ``y`` constructed at an earlier stage.
-
-Under the propositions-as-type correspondence, when ``C x`` is an element of ``Prop``, the eliminator represents a principle of induction. In order to show ``∀ x, C x``, it suffices to show that ``C`` holds for each constructor, under the inductive hypothesis that it holds for all recursive inputs to the constructor.
-
-The eliminator and constructors satisfy the following identities, in which all the arguments are shown explicitly. Suppose we set ``F := foo.rec a C f₁ ... fₙ``. Then for each constructor, we have the definitional reduction:
-
-```
-F (constructorᵢ a b) = fᵢ b ... (fun d : δᵢⱼ => F (bⱼ d)) ...
-```
-
-where the ellipses include one entry for each recursive argument.
-
-Below are some common examples of inductive types, many of which are defined in the core library.
-
-```lean
-namespace Hide
-universe u v
-
--- BEGIN
-inductive Empty : Type
-
-inductive Unit : Type
-| unit : Unit
-
-inductive Bool : Type
-| false : Bool
-| true : Bool
-
-inductive Prod (α : Type u) (β : Type v) : Type (max u v)
-| mk : α → β → Prod α β
-
-inductive Sum (α : Type u) (β : Type v)
-| inl : α → Sum α β
-| inr : β → Sum α β
-
-inductive Sigma (α : Type u) (β : α → Type v)
-| mk : (a : α) → β a → Sigma α β
-
-inductive false : Prop
-
-inductive True : Prop
-| trivial : True
-
-inductive And (p q : Prop) : Prop
-| intro : p → q → And p q
-
-inductive Or (p q : Prop) : Prop
-| inl : p → Or p q
-| inr : q → Or p q
-
-inductive Exists (α : Type u) (p : α → Prop) : Prop
-| intro : ∀ x : α, p x → Exists α p
-
-inductive Subtype (α : Type u) (p : α → Prop) : Type u
-| intro : ∀ x : α, p x → Subtype α p
-
-inductive Nat : Type
-| zero : Nat
-| succ : Nat → Nat
-
-inductive List (α : Type u)
-| nil : List α
-| cons : α → List α → List α
-
--- full binary tree with nodes and leaves labeled from α
-inductive BinTree (α : Type u)
-| leaf : α → BinTree α
-| node : BinTree α → α → BinTree α → BinTree α
-
--- every internal node has subtrees indexed by Nat
-inductive CBT (α : Type u)
-| leaf : α → CBT α
-| node : (Nat → CBT α) → CBT α
--- END
-end Hide
-```
-
-Note that in the syntax of the inductive definition ``Foo``, the context ``(a : α)`` is left implicit. In other words, constructors and recursive arguments are written as though they have return type ``Foo`` rather than ``Foo a``.
-
-Elements of the context ``(a : α)`` can be marked implicit as described in [Implicit Arguments](#implicit.md#implicit_arguments). These annotations bear only on the type former, ``Foo``. Lean uses a heuristic to determine which arguments to the constructors should be marked implicit, namely, an argument is marked implicit if it can be inferred from the type of a subsequent argument. If the annotation ``{}`` appears after the constructor, a argument is marked implicit if it can be inferred from the type of a subsequent argument *or the return type*. For example, it is useful to let ``nil`` denote the empty list of any type, since the type can usually be inferred in the context in which it appears. These heuristics are imperfect, and you may sometimes wish to define your own constructors in terms of the default ones. In that case, use the ``[match_pattern]`` [attribute](TODO: missing link) to ensure that these will be used appropriately by the [Equation Compiler](#the-equation-compiler).
-
-There are restrictions on the universe ``u`` in the return type ``Sort u`` of the type former. There are also restrictions on the universe ``u`` in the return type ``Sort u`` of the motive of the eliminator. These will be discussed in the next section in the more general setting of inductive families.
-
-Lean allows some additional syntactic conveniences. You can omit the return type of the type former, ``Sort u``, in which case Lean will infer the minimal possible nonzero value for ``u``. As with function definitions, you can list arguments to the constructors before the colon. In an enumerated type (that is, one where the constructors have no arguments), you can also leave out the return type of the constructors.
-
-```lean
-namespace Hide
-universe u
-
--- BEGIN
-inductive Weekday
-| sunday | monday | tuesday | wednesday
-| thursday | friday | saturday
-
-inductive Nat
-| zero
-| succ (n : Nat) : Nat
-
-inductive List (α : Type u)
-| nil : List α
-| cons (a : α) (l : List α) : List α
-
-@[match_pattern]
-def List.nil' (α : Type u) : List α := List.nil
-
-def length {α : Type u} : List α → Nat
-| (List.nil' _) => 0
-| (List.cons a l) => 1 + length l
--- END
-
-end Hide
-```
-
-The type former, constructors, and eliminator are all part of Lean's axiomatic foundation, which is to say, they are part of the trusted kernel. In addition to these axiomatically declared constants, Lean automatically defines some additional objects in terms of these, and adds them to the environment. These include the following:
-
-- ``Foo.recOn`` : a variant of the eliminator, in which the major premise comes first
-- ``Foo.casesOn`` : a restricted version of the eliminator which omits any recursive calls
-- ``Foo.noConfusionType``, ``Foo.noConfusion`` : functions which witness the fact that the inductive type is freely generated, i.e. that the constructors are injective and that distinct constructors produce distinct objects
-- ``Foo.below``, ``Foo.ibelow`` : functions used by the equation compiler to implement structural recursion
-- ``instance : SizeOf Foo`` : a measure which can be used for well-founded recursion
-
-Note that it is common to put definitions and theorems related to a datatype ``foo`` in a namespace of the same name. This makes it possible to use projection notation described in [Structures](struct.md#structures) and [Namespaces](namespaces.md#namespaces).
-
-```lean
-namespace Hide
-universe u
-
--- BEGIN
-inductive Nat
-| zero
-| succ (n : Nat) : Nat
-
-#check Nat
-#check @Nat.rec
-#check Nat.zero
-#check Nat.succ
-
-#check @Nat.recOn
-#check @Nat.casesOn
-#check @Nat.noConfusionType
-#check @Nat.noConfusion
-#check @Nat.brecOn
-#check Nat.below
-#check Nat.ibelow
-#check Nat._sizeOf_1
-
--- END
-
-end Hide
-```
-
-.. _inductive_families:
-
-Inductive Families
-==================
-
-In fact, Lean implements a slight generalization of the inductive types described in the previous section, namely, inductive *families*. The declaration of an inductive family in Lean has the following form:
-
-```
-inductive Foo (a : α) : Π (c : γ), Sort u
-| constructor₁ : Π (b : β₁), Foo t₁
-| constructor₂ : Π (b : β₂), Foo t₂
-...
-| constructorₙ : Π (b : βₙ), Foo tₙ
-```
-
-Here ``(a : α)`` is a context, ``(c : γ)`` is a telescope in context ``(a : α)``, each ``(b : βᵢ)`` is a telescope in the context ``(a : α)`` together with ``(Foo : Π (c : γ), Sort u)`` subject to the constraints below, and each ``tᵢ`` is a tuple of terms in the context ``(a : α) (b : βᵢ)`` having the types ``γ``. Instead of defining a single inductive type ``Foo a``, we are now defining a family of types ``Foo a c`` indexed by elements ``c : γ``.  Each constructor, ``constructorᵢ``, places its result in the type ``Foo a tᵢ``, the member of the family with index ``tᵢ``.
-
-The modifications to the scheme in the previous section are straightforward. Suppose the telescope ``(b : βᵢ)`` is ``(b₁ : βᵢ₁) ... (bᵤ : βᵢᵤ)``.
-
-- As before, an argument ``(bⱼ : βᵢⱼ)`` is *nonrecursive* if ``βᵢⱼ`` does not refer to ``Foo,`` the inductive type being defined. In that case, ``βᵢⱼ`` can be any type, so long as it does not refer to any nonrecursive arguments.
-
-- An argument ``(bⱼ : βᵢⱼ)`` is *recursive* if ``βᵢⱼ`` is of the form ``Π (d : δ), Foo s`` where ``(d : δ)`` is a telescope which does not refer to ``Foo`` or any nonrecursive arguments and ``s`` is a tuple of terms in context ``(a : α)`` and the previous nonrecursive ``bⱼ``'s with types ``γ``.
-
-The declaration of the type ``Foo`` as above results in the addition of the following constants to the environment:
-
-- the *type former* ``Foo : Π (a : α) (c : γ), Sort u``
-- for each ``i``, the *constructor* ``Foo.constructorᵢ : Π (a : α) (b : βᵢ), Foo a tᵢ``
-- the *eliminator* ``Foo.rec``, which takes arguments
-
-  + ``(a : α)`` (the parameters)
-  + ``{C : Π (c : γ), Foo a c → Type u}`` (the motive of the elimination)
-  + for each ``i``, the minor premise corresponding to ``constructorᵢ``
-  + ``(x : Foo a)`` (the major premise)
-
-  and returns an element of ``C x``. Here, The ith minor premise is a function which takes
-
-  +  ``(b : βᵢ)`` (the arguments to the constructor)
-  + an argument of type ``Π (d : δ), C s (bⱼ d)`` corresponding to each recursive argument ``(bⱼ : βᵢⱼ)``, where ``βᵢⱼ``  is of the form ``Π (d : δ), Foo s``
-
-  and returns an element of ``C tᵢ (constructorᵢ a b)``.
-
-Suppose we set ``F := Foo.rec a C f₁ ... fₙ``. Then for each constructor, we have the definitional reduction, as before:
-
-```
-F (constructorᵢ a b) = fᵢ b ... (fun d : δᵢⱼ => F (bⱼ d)) ...
-```
-
-where the ellipses include one entry for each recursive argument.
-
-The following are examples of inductive families.
-
-```lean
-namespace Hide
-universe u
-
--- BEGIN
-inductive Vector (α : Type u) : Nat → Type u
-| nil  : Vector 0
-| succ : Π n, Vector n → Vector (n + 1)
-
--- 'IsProd s n' means n is a product of elements of s
-inductive IsProd (s : Set Nat) : Nat → Prop
-| base : ∀ n ∈ s, IsProd n
-| step : ∀ m n, IsProd m → IsProd n → IsProd (m * n)
-
-inductive Eq {α : Sort u} (a : α) : α → Prop
-| refl : Eq a
--- END
-
-end Hide
-```
-
-We can now describe the constraints on the return type of the type former, ``Sort u``. We can always take ``u`` to be ``0``, in which case we are defining an inductive family of propositions. If ``u`` is nonzero, however, it must satisfy the following constraint: for each type ``βᵢⱼ : Sort v`` occurring in the constructors, we must have ``u ≥ v``. In the set-theoretic interpretation, this ensures that the universe in which the resulting type resides is large enough to contain the inductively generated family, given the number of distinctly-labeled constructors. The restriction does not hold for inductively defined propositions, since these contain no data.
-
-Putting an inductive family in ``Prop``, however, does impose a restriction on the eliminator. Generally speaking, for an inductive family in ``Prop``, the motive in the eliminator is required to be in ``Prop``. But there is an exception to this rule: you are allowed to eliminate from an inductively defined ``Prop`` to an arbitrary ``Sort`` when there is only one constructor, and each argument to that constructor is either in ``Prop`` or an index. The intuition is that in this case the elimination does not make use of any information that is not already given by the mere fact that the type of argument is inhabited. This special case is known as *singleton elimination*.
-
-.. _mutual_and_nested_inductive_definitions:
-
-Mutual and Nested Inductive Definitions
-=======================================
-
-Lean supports two generalizations of the inductive families described above, namely, *mutual* and *nested* inductive definitions. These are *not* implemented natively in the kernel. Rather, the definitions are compiled down to the primitive inductive types and families.
-
-The first generalization allows for multiple inductive types to be defined simultaneously.
-
-```
-mutual
-
-inductive Foo (a : α) : Π (c : γ₁), Sort u
-| constructor₁₁ : Π (b : β₁₁), Foo a t₁₁
-| constructor₁₂ : Π (b : β₁₂), Foo a t₁₂
-...
-| constructor₁ₙ : Π (b : β₁ₙ), Foo a t₁ₙ
-
-inductive Bar (a : α) : Π (c : γ₂), Sort u
-| constructor₂₁ : Π (b : β₂₁), Bar a t₂₁
-| constructor₂₂ : Π (b : β₂₂), Bar a t₂₂
-...
-| constructor₂ₘ : Π (b : β₂ₘ), Bar a t₂ₘ
-
-end
-```
-
-Here the syntax is shown for defining two inductive families, ``Foo`` and ``Bar``, but any number is allowed. The restrictions are almost the same as for ordinary inductive families. For example, each ``(b : βᵢⱼ)`` is a telescope relative to the context ``(a : α)``. The difference is that the constructors can now have recursive arguments whose return types are any of the inductive families currently being defined, in this case ``Foo`` and ``Bar``. Note that all of the inductive definitions share the same parameters ``(a : α)``, though they may have different indices.
-
-A mutual inductive definition is compiled down to an ordinary inductive definition using an extra finite-valued index to distinguish the components. The details of the internal construction are meant to be hidden from most users. Lean defines the expected type formers ``Foo`` and ``Bar`` and constructors ``constructorᵢⱼ`` from the internal inductive definition. There is no straightforward elimination principle, however. Instead, Lean defines an appropriate ``sizeOf`` measure, meant for use with well-founded recursion, with the property that the recursive arguments to a constructor are smaller than the constructed value.
-
-The second generalization relaxes the restriction that in the recursive definition of ``Foo``, ``Foo`` can only occur strictly positively in the type of any of its recursive arguments. Specifically, in a nested inductive definition, ``Foo`` can appear as an argument to another inductive type constructor, so long as the corresponding parameter occurs strictly positively in the constructors for *that* inductive type. This process can be iterated, so that additional type constructors can be applied to those, and so on.
-
-A nested inductive definition is compiled down to an ordinary inductive definition using a mutual inductive definition to define copies of all the nested types simultaneously. Lean then constructs isomorphisms between the mutually defined nested types and their independently defined counterparts. Once again, the internal details are not meant to be manipulated by users. Rather, the type former and constructors are made available and work as expected, while an appropriate ``sizeOf`` measure is generated for use with well-founded recursion.
-
-```lean
-universe u
--- BEGIN
-mutual
-inductive Even : Nat → Prop
-| even_zero : Even 0
-| even_succ : ∀ n, Odd n → Even (n + 1)
-inductive Odd : Nat → Prop
-| odd_succ : ∀ n, Even n → Odd (n + 1)
-end
-
-inductive Tree (α : Type u)
-| mk : α → List (Tree α) → Tree α
-
-inductive DoubleTree (α : Type u)
-| mk : α → List (DoubleTree α) × List (DoubleTree α) → DoubleTree α
--- END
-```
-
-.. _the_equation_compiler:
-
-The Equation Compiler
-=====================
-
-The equation compiler takes an equational description of a function or proof and tries to define an object meeting that specification. It expects input with the following syntax:
-
-```
-def foo (a : α) : Π (b : β), γ
-| [patterns₁] => t₁
-...
-| [patternsₙ] => tₙ
-```
-
-Here ``(a : α)`` is a telescope, ``(b : β)`` is a telescope in the context ``(a : α)``, and ``γ`` is an expression in the context ``(a : α) (b : β)`` denoting a ``Type`` or a ``Prop``.
-
-Each ``patternsᵢ`` is a sequence of patterns of the same length as ``(b : β)``. A pattern is either:
-
-- a variable, denoting an arbitrary value of the relevant type,
-- an underscore, denoting a *wildcard* or *anonymous variable*,
-- an inaccessible term (see below), or
-- a constructor for the inductive type of the corresponding argument, applied to a sequence of patterns.
-
-In the last case, the pattern must be enclosed in parentheses.
-
-Each term ``tᵢ`` is an expression in the context ``(a : α)`` together with the variables introduced on the left-hand side of the token ``=>``. The term ``tᵢ`` can also include recursive calls to ``foo``, as described below. The equation compiler does case splitting on the variables ``(b : β)`` as necessary to match the patterns, and defines ``foo`` so that it has the value ``tᵢ`` in each of the cases. In ideal circumstances (see below), the equations hold definitionally. Whether they hold definitionally or only propositionally, the equation compiler proves the relevant equations and assigns them internal names. They are accessible by the ``rewrite`` and ``simp`` tactics under the name ``foo`` (see [Rewrite](tactics.md#rewrite) and _[TODO: where is simplifier tactic documented?]_. If some of the patterns overlap, the equation compiler interprets the definition so that the first matching pattern applies in each case. Thus, if the last pattern is a variable, it covers all the remaining cases. If the patterns that are presented do not cover all possible cases, the equation compiler raises an error.
-
-When identifiers are marked with the ``[match_pattern]`` attribute, the equation compiler unfolds them in the hopes of exposing a constructor. For example, this makes it possible to write ``n+1`` and ``0`` instead of ``Nat.succ n`` and ``Nat.zero`` in patterns.
-
-For a nonrecursive definition involving case splits, the defining equations will hold definitionally. With inductive types like ``Char``, ``String``, and ``Fin n``, a case split would produce definitions with an inordinate number of cases. To avoid this, the equation compiler uses ``if ... then ... else`` instead of ``casesOn`` when defining the function. In this case, the defining equations hold definitionally as well.
-
-```lean
-open Nat
-
-def sub2 : Nat → Nat
-| zero          => 0
-| succ zero     => 0
-| succ (succ a) => a
-
-def bar : Nat → List Nat → Bool → Nat
-| 0,   _,      false => 0
-| 0,   b :: _, _     => b
-| 0,   [],     true  => 7
-| a+1, [],     false => a
-| a+1, [],     true  => a + 1
-| a+1, b :: _, _     => a + b
-
-def baz : Char → Nat
-| 'A' => 1
-| 'B' => 2
-| _   => 3
-```
-
-If any of the terms ``tᵢ`` in the template above contain a recursive call to ``foo``, the equation compiler tries to interpret the definition as a structural recursion. In order for that to succeed, the recursive arguments must be subterms of the corresponding arguments on the left-hand side. The function is then defined using a *course of values* recursion, using automatically generated functions ``below`` and ``brec`` in the namespace corresponding to the inductive type of the recursive argument. In this case the defining equations hold definitionally, possibly with additional case splits.
-
-```lean
-namespace Hide
-
--- BEGIN
-def fib : Nat → Nat
-| 0     => 1
-| 1     => 1
-| (n+2) => fib (n+1) + fib n
-
-def append {α : Type} : List α → List α → List α
-| [],   l => l
-| h::t, l => h :: append t l
-
-example : append [(1 : Nat), 2, 3] [4, 5] = [1, 2, 3, 4, 5] => rfl
--- END
-
-end Hide
-```
-
-If structural recursion fails, the equation compiler falls back on well-founded recursion. It tries to infer an instance of ``SizeOf`` for the type of each argument, and then show that each recursive call is decreasing under the lexicographic order of the arguments with respect to ``sizeOf`` measure. If it fails, the error message provides information as to the goal that Lean tried to prove. Lean uses information in the local context, so you can often provide the relevant proof manually using ``have`` in the body of the definition. In this case of well-founded recursion, the defining equations hold only propositionally, and can be accessed using ``simp`` and ``rewrite`` with the name ``foo``.
-
-```lean
-namespace Hide
-open Nat
-
--- BEGIN
-def div : Nat → Nat → Nat
-| x, y =>
-  if h : 0 < y ∧ y ≤ x then
-    have : x - y < x :=
-      sub_lt (Nat.lt_of_lt_of_le h.left h.right) h.left
-    div (x - y) y + 1
-  else
-    0
-
-example (x y : Nat) :
-  div x y = if 0 < y ∧ y ≤ x then div (x - y) y + 1 else 0 :=
-by rw [div]; rfl
--- END
-
-end Hide
-```
-
-Note that recursive definitions can in general require nested recursions, that is, recursion on different arguments of ``foo`` in the template above. The equation compiler handles this by abstracting later arguments, and recursively defining higher-order functions to meet the specification.
-
-The equation compiler also allows mutual recursive definitions, with a syntax similar to that of [Mutual and Nested Inductive Definitions](#mutual-and-nested-inductive-definitions). They are compiled using well-founded recursion, and so once again the defining equations hold only propositionally.
-
-```lean
-mutual
-def even : Nat → Bool
-| 0   => true
-| a+1 => odd a
-def odd : Nat → Bool
-| 0   => false
-| a+1 => even a
-end
-
-example (a : Nat) : even (a + 1) = odd a :=
-by simp [even]
-
-example (a : Nat) : odd (a + 1) = even a :=
-by simp [odd]
-```
-
-Well-founded recursion is especially useful with [Mutual and Nested Inductive Definitions](#mutual-and-nested-inductive-definitions), since it provides the canonical way of defining functions on these types.
-
-```lean
-mutual
-inductive Even : Nat → Prop
-| even_zero : Even 0
-| even_succ : ∀ n, Odd n → Even (n + 1)
-inductive Odd : Nat → Prop
-| odd_succ : ∀ n, Even n → Odd (n + 1)
-end
-
-open Even Odd
-
-theorem not_odd_zero : ¬ Odd 0 := fun x => nomatch x
-
-mutual
-theorem even_of_odd_succ : ∀ n, Odd (n + 1) → Even n
-| _, odd_succ n h => h
-theorem odd_of_even_succ : ∀ n, Even (n + 1) → Odd n
-| _, even_succ n h => h
-end
-
-inductive Term
-| const : String → Term
-| app   : String → List Term → Term
-
-open Term
-
-mutual
-def num_consts : Term → Nat
-| .const n  => 1
-| .app n ts => num_consts_lst ts
-def num_consts_lst : List Term → Nat
-| []    => 0
-| t::ts => num_consts t + num_consts_lst ts
-end
-```
-
-The case where patterns are matched against an argument whose type is an inductive family is known as *dependent pattern matching*. This is more complicated, because the type of the function being defined can impose constraints on the patterns that are matched. In this case, the equation compiler will detect inconsistent cases and rule them out.
-
-```lean
-universe u
-
-inductive Vector (α : Type u) : Nat → Type u
-| nil  : Vector α 0
-| cons : α → Vector α n → Vector α (n+1)
-
-namespace Vector
-
-def head {α : Type} : Vector α (n+1) → α
-| cons h t => h
-
-def tail {α : Type} : Vector α (n+1) → Vector α n
-| cons h t => t
-
-def map {α β γ : Type} (f : α → β → γ) :
-  ∀ {n}, Vector α n → Vector β n → Vector γ n
-| 0,   nil,       nil       => nil
-| n+1, cons a va, cons b vb => cons (f a b) (map f va vb)
-
-end Vector
-```
-
-.. _match_expressions:
-
-Match Expressions
-=================
-
-Lean supports a ``match ... with ...`` construct similar to ones found in most functional programming languages. The syntax is as follows:
-
-```
-match t₁, ..., tₙ with
-| p₁₁, ..., p₁ₙ => s₁
-...
-| pₘ₁, ..., pₘₙ => sₘ
-```
-
-Here ``t₁, ..., tₙ`` are any terms in the context in which the expression appears, the expressions ``pᵢⱼ`` are patterns, and the terms ``sᵢ`` are expressions in the local context together with variables introduced by the patterns on the left-hand side. Each ``sᵢ`` should have the expected type of the entire ``match`` expression.
-
-Any ``match`` expression is interpreted using the equation compiler, which generalizes ``t₁, ..., tₙ``, defines an internal function meeting the specification, and then applies it to ``t₁, ..., tₙ``. In contrast to the definitions in [The Equation Compiler](declarations.md#the-equation-compiler), the terms ``tᵢ`` are arbitrary terms rather than just variables, and the expression can occur anywhere within a Lean expression, not just at the top level of a definition. Note that the syntax here is somewhat different: both the terms ``tᵢ`` and the patterns ``pᵢⱼ`` are separated by commas.
-
-```lean
-def foo (n : Nat) (b c : Bool) :=
-5 + match n - 5, b && c with
-    | 0,   true  => 0
-    | m+1, true  => m + 7
-    | 0,   false => 5
-    | m+1, false => m + 3
-```
-
-When a ``match`` has only one line, Lean provides alternative syntax with a destructuring ``let``, as well as a destructuring lambda abstraction. Thus the following definitions all have the same net effect.
-
-```lean
-def bar₁ : Nat × Nat → Nat
-| (m, n) => m + n
-
-def bar₂ (p : Nat × Nat) : Nat :=
-match p with | (m, n) => m + n
-
-def bar₃ : Nat × Nat → Nat :=
-fun ⟨m, n⟩ => m + n
-
-def bar₄ (p : Nat × Nat) : Nat :=
-let ⟨m, n⟩ := p; m + n
-```
-
-Information about the term being matched can be preserved in each branch using the syntax `match h : t with`. For example, a user may want to match a term `ns ++ ms : List Nat`, while tracking the hypothesis `ns ++ ms = []` or `ns ++ ms= h :: t` in the respective match arm:
-
-```lean
-def foo (ns ms : List Nat) (h1 : ns ++ ms ≠ []) (k : Nat -> Char) : Char :=
-  match h2 : ns ++ ms with
-  -- in this arm, we have the hypothesis `h2 : ns ++ ms = []`
-  | [] => absurd h2 h1
-  -- in this arm, we have the hypothesis `h2 : ns ++ ms = h :: t`
-  | h :: t => k h
-
--- '7'
-#eval foo [7, 8, 9] [] (by decide) Nat.digitChar
-```
-
-.. _structures_and_records:
-
-Structures and Records
-======================
-
-The ``structure`` command in Lean is used to define an inductive data type with a single constructor and to define its projections at the same time. The syntax is as follows:
-
-```
-structure Foo (a : α) extends Bar, Baz : Sort u :=
-constructor :: (field₁ : β₁) ... (fieldₙ : βₙ)
-```
-
-Here ``(a : α)`` is a telescope, that is, the parameters to the inductive definition. The name ``constructor`` followed by the double colon is optional; if it is not present, the name ``mk`` is used by default. The keyword ``extends`` followed by a list of previously defined structures is also optional; if it is present, an instance of each of these structures is included among the fields to ``Foo``, and the types ``βᵢ`` can refer to their fields as well. The output type, ``Sort u``, can be omitted, in which case Lean infers to smallest non-``Prop`` sort possible. Finally, ``(field₁ : β₁) ... (fieldₙ : βₙ)`` is a telescope relative to ``(a : α)`` and the fields in ``bar`` and ``baz``.
-
-The declaration above is syntactic sugar for an inductive type declaration, and so results in the addition of the following constants to the environment:
-
-- the type former : ``Foo : Π (a : α), Sort u``
-- the single constructor :
-
-```
-Foo.constructor : Π (a : α) (toBar : Bar) (toBaz : Baz)
-  (field₁ : β₁) ... (fieldₙ : βₙ), Foo a
-```
-
-- the eliminator ``Foo.rec`` for the inductive type with that constructor
-
-In addition, Lean defines
-
-- the projections : ``fieldᵢ : Π (a : α) (c : Foo) : βᵢ`` for each ``i``
-
-where any other fields mentioned in ``βᵢ`` are replaced by the relevant projections from ``c``.
-
-Given ``c : Foo``, Lean offers the following convenient syntax for the projection ``Foo.fieldᵢ c``:
-
-- *anonymous projections* : ``c.fieldᵢ``
-- *numbered projections* : ``c.i``
-
-These can be used in any situation where Lean can infer that the type of ``c`` is of the form ``Foo a``. The convention for anonymous projections is extended to any function ``f`` defined in the namespace ``Foo``, as described in [Namespaces](namespaces.md).
-
-Similarly, Lean offers the following convenient syntax for constructing elements of ``Foo``. They are equivalent to ``Foo.constructor b₁ b₂ f₁ f₁ ... fₙ``, where ``b₁ : Bar``, ``b₂ : Baz``, and each ``fᵢ : βᵢ`` :
-
-- *anonymous constructor*: ``⟨ b₁, b₂, f₁, ..., fₙ ⟩``
-- *record notation*:
-
-```
-{ toBar := b₁, toBaz := b₂, field₁ := f₁, ...,
-    fieldₙ := fₙ :  Foo a }
-```
-
-The anonymous constructor can be used in any context where Lean can infer that the expression should have a type of the form ``Foo a``. The unicode brackets are entered as ``\<`` and ``\>`` respectively.
-
-When using record notation, you can omit the annotation ``: Foo a`` when Lean can infer that the expression should have a type of the form ``Foo a``. You can replace either ``toBar`` or ``toBaz`` by assignments to *their* fields as well, essentially acting as though the fields of ``Bar`` and ``Baz`` are simply imported into ``Foo``. Finally, record notation also supports
-
-- *record updates*: ``{ t with ... fieldᵢ := fᵢ ...}``
-
-Here ``t`` is a term of type ``Foo a`` for some ``a``. The notation instructs Lean to take values from ``t`` for any field assignment that is omitted from the list.
-
-Lean also allows you to specify a default value for any field in a structure by writing ``(fieldᵢ : βᵢ := t)``. Here ``t`` specifies the value to use when the field ``fieldᵢ`` is left unspecified in an instance of record notation.
-
-```lean
-universe u v
-
-structure Vec (α : Type u) (n : Nat) :=
-(l : List α) (h : l.length = n)
-
-structure Foo (α : Type u) (β : Nat → Type v) : Type (max u v) :=
-(a : α) (n : Nat) (b : β n)
-
-structure Bar :=
-(c : Nat := 8) (d : Nat)
-
-structure Baz extends Foo Nat (Vec Nat), Bar :=
-(v : Vec Nat n)
-
-#check Foo
-#check @Foo.mk
-#check @Foo.rec
-
-#check Foo.a
-#check Foo.n
-#check Foo.b
-
-#check Baz
-#check @Baz.mk
-#check @Baz.rec
-
-#check Baz.toFoo
-#check Baz.toBar
-#check Baz.v
-
-def bzz := Vec.mk [1, 2, 3] rfl
-
-#check Vec.l bzz
-#check Vec.h bzz
-#check bzz.l
-#check bzz.h
-#check bzz.1
-#check bzz.2
-
-example : Vec Nat 3 := Vec.mk [1, 2, 3] rfl
-example : Vec Nat 3 := ⟨[1, 2, 3], rfl⟩
-example : Vec Nat 3 := { l := [1, 2, 3], h := rfl : Vec Nat 3 }
-example : Vec Nat 3 := { l := [1, 2, 3], h := rfl }
-
-example : Foo Nat (Vec Nat) := ⟨1, 3, bzz⟩
-
-example : Baz := ⟨⟨1, 3, bzz⟩, ⟨5, 7⟩, bzz⟩
-example : Baz := { a := 1, n := 3, b := bzz, c := 5, d := 7, v := bzz}
-def fzz : Foo Nat (Vec Nat) := {a := 1, n := 3, b := bzz}
-
-example : Foo Nat (Vec Nat) := { fzz with a := 7 }
-example : Baz := { fzz with c := 5, d := 7, v := bzz }
-
-example : Bar := { c := 8, d := 9 }
-example : Bar := { d := 9 }  -- uses the default value for c
-```
-
-.. _type_classes:
-
-Type Classes
-============
-
-(Classes and instances. Anonymous instances. Local instances.)
-
-
-.. [Dybjer] Dybjer, Peter, *Inductive Families*. Formal Aspects of Computing 6, 1994, pages 440-465.

doc/dev/bootstrap.md

@@ -1,122 +0,0 @@
-# Lean Build Bootstrapping
-
-Since version 4, Lean is a partially bootstrapped program: most parts of the
-frontend and compiler are written in Lean itself and thus need to be built before
-building Lean itself - which is needed to again build those parts. This cycle is
-broken by using pre-built C files checked into the repository (which ultimately
-go back to a point where the Lean compiler was not written in Lean) in place of
-these Lean inputs and then compiling everything in multiple stages up to a fixed
-point. The build directory is organized in these stages:
-
-```bash
-stage0/
-  # Bootstrap binary built from stage0/src/.
-  # We do not use any other files from this directory in further stages.
-  bin/lean
-stage1/
-  include/
-    config.h  # config variables used to build `lean` such as used allocator
-    runtime/lean.h  # runtime header, used by extracted C code, uses `config.h`
-  share/lean/
-    lean.mk  # used by `leanmake`
-  lib/
-    lean/**/*.olean  # the Lean library (incl. the compiler) compiled by the previous stage's `lean`
-    temp/**/*.{c,o}  # the library extracted to C and compiled by `leanc`
-    libInit.a libLean.a  # static libraries of the Lean library
-    libleancpp.a  # a static library of the C++ sources of Lean
-    libleanshared.so  # a dynamic library including the static libraries above
-  bin/
-    lean  # the Lean compiler & server, a small executable that calls directly into libleanshared.so
-    leanc  # a wrapper around a C compiler supplying search paths etc
-    leanmake  # a wrapper around `make` supplying the Makefile above
-stage2/...
-stage3/...
-```
-
-Stage 0 can be viewed as a blackbox since it does not depend on any local
-changes and is equivalent to downloading a bootstrapping binary as done in other
-compilers. The build for any other stage starts by building the runtime and
-standard library from `src/`, using the `lean` binary from the previous stage in
-the latter case, which are then assembled into a new `bin/lean` binary.
-
-Each stage can be built by calling `make stageN` in the root build folder.
-Running just `make` will default to stage 1, which is usually sufficient for
-testing changes on the test suite or other files outside of the stdlib. However,
-it might happen that the stage 1 compiler is not able to load its own stdlib,
-e.g. when changing the .olean format: the stage 1 stdlib will use the format
-generated by the stage 0 compiler, but the stage 1 compiler will expect the new
-format. In this case, we should continue with building and testing stage 2
-instead, which will both build and expect the new format. Note that this is only
-possible because when building a stage's stdlib, we use the previous compiler
-but never load the previous stdlib (since everything is `prelude`). We can also
-use stage 2 to test changes in the compiler or other "meta" parts, i.e. changes
-that affect the produced (.olean or .c) code, on the stdlib and compiler itself.
-We are not aware of any "meta-meta" parts that influence more than two stages of
-compilation, so stage 3 should always be identical to stage 2 and only exists as
-a sanity check.
-
-In summary, doing a standard build via `make` internally involves these steps:
-
-1. compile the `stage0/src` archived sources into `stage0/bin/lean`
-1. use it to compile the current library (*including* your changes) into `stage1/lib`
-1. link that and the current C++ code from `src/` into `stage1/bin/lean`
-
-You now have a Lean binary and library that include your changes, though their
-own compilation was not influenced by them, that you can use to test your
-changes on test programs whose compilation *will* be influenced by the changes.
-
-Finally, when we want to use new language features in the library, we need to
-update the stage 0 compiler, which can be done via `make -C stageN update-stage0`.
-`make update-stage0` without `-C` defaults to stage1.
-
-## Further Bootstrapping Complications
-
-As written above, changes in meta code in the current stage usually will only
-affect later stages. This is an issue in two specific cases.
-
-* For *non-builtin* meta code such as `notation`s or `macro`s in
-  `Notation.lean`, we expect changes to affect the current file and all later
-  files of the same stage immediately, just like outside the stdlib. To ensure
-  this, we need to build the stage using `-Dinterpreter.prefer_native=false` -
-  otherwise, when executing a macro, the interpreter would notice that there is
-  already a native symbol available for this function and run it instead of the
-  new IR, but the symbol is from the previous stage!
-
-  To make matters more complicated, while `false` is a reasonable default
-  incurring only minor overhead (`ParserDescr`s and simple macros are cheap to
-  interpret), there are situations where we *need* to set the option to `true`:
-  when the interpreter is executed from the native code of the previous stage,
-  the type of the value it computes must be identical to/ABI-compatible with the
-  type in the previous stage. For example, if we add a new parameter to `Macro`
-  or reorder constructors in `ParserDescr`, building the stage with the
-  interpreter will likely fail. Thus we need to set `interpreter.prefer_native`
-  to `true` in such cases to "freeze" meta code at their versions in the
-  previous stage; no new meta code should be introduced in this stage. Any
-  further stages (e.g. after an `update-stage0`) will then need to be compiled
-  with the flag set to `false` again since they will expect the new signature.
-
-  For an example, see https://github.com/leanprover/lean4/commit/da4c46370d85add64ef7ca5e7cc4638b62823fbb.
-
-* For the special case of *quotations*, it is desirable to have changes in
-  built-in parsers affect them immediately: when the changes in the parser
-  become active in the next stage, macros implemented via quotations should
-  generate syntax trees compatible with the new parser, and quotation patterns
-  in macro and elaborators should be able to match syntax created by the new
-  parser and macros. Since quotations capture the syntax tree structure during
-  execution of the current stage and turn it into code for the next stage, we
-  need to run the current stage's built-in parsers in quotation via the
-  interpreter for this to work. Caveats:
-  * Since interpreting full parsers is not nearly as cheap and we rarely change
-    built-in syntax, this needs to be opted in using `-Dinternal.parseQuotWithCurrentStage=true`.
-  * The parser needs to be reachable via an `import` statement, otherwise the
-    version of the previous stage will silently be used.
-  * Only the parser code (`Parser.fn`) is affected; all metadata such as leading
-    tokens is taken from the previous stage.
-
-  For an example, see https://github.com/leanprover/lean4/commit/f9dcbbddc48ccab22c7674ba20c5f409823b4cc1#diff-371387aed38bb02bf7761084fd9460e4168ae16d1ffe5de041b47d3ad2d22422
-  (from before the flag defaulted to `false`).
-
-To modify either of these flags both for building and editing the stdlib, adjust
-the code in `stage0/src/stdlib_flags.h`. The flags will automatically be reset
-on the next `update-stage0` when the file is overwritten with the original
-version in `src/`.

doc/dev/ffi.md

@@ -1,122 +0,0 @@
-# Foreign Function Interface
-
-NOTE: The current interface was designed for internal use in Lean and should be considered **unstable**.
-It will be refined and extended in the future.
-
-As Lean is written partially in Lean itself and partially in C++, it offers efficient interoperability between the two languages (or rather, between Lean and any language supporting C interfaces).
-This support is however currently limited to transferring Lean data types; in particular, it is not possible yet to pass or return compound data structures such as C `struct`s by value from or to Lean.
-
-There are two primary attributes for interoperating with other languages:
-* `@[extern "sym"] constant leanSym : ...` binds a Lean declaration to the external symbol `sym`.
-  It can also be used with `def` to provide an internal definition, but ensuring consistency of both definitions is up to the user.
-* `@[export sym] def leanSym : ...` exports `leanSym` under the unmangled symbol name `sym`.
-
-## The Lean ABI
-
-The Lean Application Binary Interface (ABI) describes how the signature of a Lean declaration is encoded as a native calling convention.
-It is based on the standard C ABI and calling convention of the target platform.
-For a Lean declaration marked with either `@[extern "sym"]` or `@[export sym]` for some symbol name `sym`, let `α₁ → ... → αₙ → β` be the normalized declaration's type.
-If `n` is 0, the corresponding C declaration is
-```c
-extern s sym;
-```
-where `s` is the C translation of `β` as specified in the next section.
-In the case of an `@[extern]` definition, the symbol's value is guaranteed to be initialized only after calling the Lean module's initializer or that of an importing module; see [Initialization](#initialization).
-
-If `n` is greater than 0, the corresponding C declaration is
-```c
-s sym(t₁, ..., tₘ);
-```
-where the parameter types `tᵢ` are the C translation of the `αᵢ` as in the next section.
-In the case of `@[extern]` all *irrelevant* types are removed first; see next section.
-
-### Translating Types from Lean to C
-
-* The integer types `UInt8`, ..., `UInt64`, `USize` are represented by the C types `uint8_t`, ..., `uint64_t`, `size_t`, respectively
-* `Char` is represented by `uint32_t`
-* `Float` is represented by `double`
-* An *enum* inductive type of at least 2 and at most 2^32 constructors, each of which with no parameters, is represented by the first type of `uint8_t`, `uint16_t`, `uint32_t` that is sufficient to represent all constructor indices.
-
-  For example, the type `Bool` is represented as `uint8_t` with values `0` for `false` and `1` for `true`.
-* `Decidable α` is represented the same way as `Bool`
-* An inductive type with a *trivial structure*, that is,
-  * it is none of the types described above
-  * it is not marked `unsafe`
-  * it has a single constructor with a single parameter of *relevant* type
-
-  is represented by the representation of that parameter's type.
-
-  For example, `{ x : α // p }`, the `Subtype` structure of a value of type `α` and an irrelevant proof, is represented by the representation of `α`.
-* `Nat` is represented by `lean_object *`.
-  Its runtime value is either a pointer to an opaque bignum object or, if the lowest bit of the "pointer" is 1 (`lean_is_scalar`), an encoded unboxed natural number (`lean_box`/`lean_unbox`).
-* A universe `Sort u`, type constructor `... → Sort u`, or proposition `p : Prop` is *irrelevant* and is either statically erased (see above) or represented as a `lean_object *` with the runtime value `lean_box(0)`
-* Any other type is represented by `lean_object *`.
-  Its runtime value is a pointer to an object of a subtype of `lean_object` (see respective declarations in `lean.h`) or the unboxed value `lean_box(cidx)` for the `cidx`th constructor of an inductive type if this constructor does not have any relevant parameters.
-
-  Example: the runtime value of `u : Unit` is always `lean_box(0)`.
-
-### Borrowing
-
-By default, all `lean_object *` parameters of an `@[extern]` function are considered *owned*, i.e. the external code is passed a "virtual RC token" and is responsible for passing this token along to another consuming function (exactly once) or freeing it via `lean_dec`.
-To reduce reference counting overhead, parameters can be marked as *borrowed* by prefixing their type with `@&`.
-Borrowed objects must only be passed to other non-consuming functions (arbitrarily often) or converted to owned values using `lean_inc`.
-In `lean.h`, the `lean_object *` aliases `lean_obj_arg` and `b_lean_obj_arg` are used to mark this difference on the C side.
-
-Return values and `@[export]` parameters are always owned at the moment.
-
-## Initialization
-
-When including Lean code as part of a larger program, modules must be *initialized* before accessing any of their declarations.
-Module initialization entails
-* initialization of all "constants" (nullary functions), including closed terms lifted out of other functions
-* execution of all `[init]` functions
-* execution of all `[builtin_init]` functions, if the `builtin` parameter of the module initializer has been set
-
-The module initializer is automatically run with the `builtin` flag for executables compiled from Lean code and for "plugins" loaded with `lean --plugin`.
-For all other modules imported by `lean`, the initializer is run without `builtin`.
-Thus `[init]` functions are run iff their module is imported, regardless of whether they have native code available or not, while `[builtin_init]` functions are only run for native executable or plugins, regardless of whether their module is imported or not.
-`lean` uses built-in initializers for e.g. registering basic parsers that should be available even without importing their module (which is necessary for bootstrapping).
-
-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.
-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();
-lean_object * initialize_A_B(uint8_t builtin, lean_object *);
-lean_object * initialize_C(uint8_t builtin, lean_object *);
-...
-
-lean_initialize_runtime_module();
-//lean_initialize();  // necessary if you (indirectly) access the `Lean` package
-
-lean_object * res;
-// use same default as for Lean executables
-uint8_t builtin = 1;
-res = initialize_A_B(builtin, lean_io_mk_world());
-if (lean_io_result_is_ok(res)) {
-    lean_dec_ref(res);
-} else {
-    lean_io_result_show_error(res);
-    lean_dec(res);
-    return ...;  // do not access Lean declarations if initialization failed
-}
-res = initialize_C(builtin, lean_io_mk_world());
-if (lean_io_result_is_ok(res)) {
-...
-
-//lean_init_task_manager();  // necessary if you (indirectly) use `Task`
-lean_io_mark_end_initialization();
-```
-
-## `@[extern]` in the Interpreter
-
-The interpreter can run Lean declarations for which symbols are available in loaded shared libraries, which includes `@[extern]` declarations.
-Thus to e.g. run `#eval` on such a declaration, you need to
-1. compile (at least) the module containing the declaration and its dependencies into a shared library, and then
-1. pass this library to `lean --load-dynlib=` to run code `import`ing this module.
-
-Note that it is not sufficient to load the foreign library containing the external symbol because the interpreter depends on code that is emitted for each `@[extern]` declaration.
-Thus it is not possible to interpret an `@[extern]` declaration in the same file.
-
-See `tests/compiler/foreign` for an example.

doc/dev/index.md

@@ -1,59 +0,0 @@
-# Development Workflow
-
-If you want to make changes to Lean itself, start by [building Lean](../make/index.html) from a clean checkout to make sure that everything is set up correctly.
-After that, read on below to find out how to set up your editor for changing the Lean source code, followed by further sections of the development manual where applicable such as on the [test suite](testing.md) and [commit convention](commit_convention.md).
-
-If you are planning to make any changes that may affect the compilation of Lean itself, e.g. changes to the parser, elaborator, or compiler, you should first read about the [bootstrapping pipeline](bootstrap.md).
-You should not edit the `stage0` directory except using the commands described in that section when necessary.
-
-## Development Setup
-
-You can use any of the [supported editors](../setup.md) for editing the Lean source code.
-If you set up `elan` as below, opening `src/` as a *workspace folder* should ensure that stage 0 (i.e. the stage that first compiles `src/`) will be used for files in that directory.
-
-### Dev setup using elan
-
-You can use [`elan`](https://github.com/leanprover/elan) to easily
-switch between stages and build configurations based on the current
-directory, both for the `lean`, `leanc`, and `leanmake` binaries in your shell's
-PATH and inside your editor.
-
-To install elan, you can do so, without installing a default version of Lean, using (Unix)
-
-```bash
-curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none
-```
-or (Windows)
-```
-curl -O --location https://raw.githubusercontent.com/leanprover/elan/master/elan-init.ps1
-powershell -f elan-init.ps1 --default-toolchain none
-del elan-init.ps1
-```
-
-You can use `elan toolchain link` to give a specific stage build
-directory a reference name, then use `elan override set` to associate
-such a name to the current directory. We usually want to use `stage0`
-for editing files in `src` and `stage1` for everything else (e.g.
-tests).
-```bash
-# in the Lean rootdir
-elan toolchain link lean4 build/release/stage1
-elan toolchain link lean4-stage0 build/release/stage0
-# make `lean` etc. point to stage1 in the rootdir and subdirs
-elan override set lean4
-cd src
-# make `lean` etc. point to stage0 anywhere inside `src`
-elan override set lean4-stage0
-```
-
-You can also use the `+toolchain` shorthand (e.g. `lean +lean4-debug`) to switch
-toolchains on the spot. `lean4-mode` will automatically use the `lean` executable
-associated with the directory of the current file as long as `lean4-rootdir` is
-unset and `~/.elan/bin` is in your `exec-path`. Where Emacs sources the
-`exec-path` from can be a bit unclear depending on your configuration, so
-alternatively you can also set `lean4-rootdir` to `"~/.elan"` explicitly.
-
-You might find that debugging through elan, e.g. via `gdb lean`, disables some
-things like symbol autocompletion because at first only the elan proxy binary
-is loaded. You can instead pass the explicit path to `bin/lean` in your build
-folder to gdb, or use `gdb $(elan which lean)`.

doc/dev/mdbook.md

@@ -1,109 +0,0 @@
-# Documentation
-
-The Lean `doc` folder contains the [Lean Manual](https://leanprover.github.io/lean4/doc/) and is
-authored in a combination of markdown (`*.md`) files and literate Lean files.  The .lean files are
-preprocessed using a tool called [LeanInk](https://github.com/leanprover/leanink) and
-[Alectryon](https://github.com/Kha/alectryon) which produces a generated markdown file.  We then run
-`mdbook` on the result to generate the html pages.
-
-
-## Settings
-
-We are using the following settings while editing the markdown docs.
-
-```json
-{
-    "files.insertFinalNewline": true,
-    "files.trimTrailingWhitespace": true,
-    "[markdown]": {
-        "rewrap.wrappingColumn": 70
-    }
-}
-```
-
-## Build
-
-### Using Nix
-
-Building the manual using Nix (which is what the CI does) is as easy as
-```bash
-$ nix build --update-input lean ./doc
-```
-You can also open a shell with `mdbook` for running the commands mentioned below with
-`nix develop ./doc#book`. Otherwise, read on.
-
-### Manually
-
-To build and test the book you have to preprocess the .lean files with Alectryon then use our own
-fork of the Rust tool named [mdbook](https://github.com/leanprover/mdbook). We have our own fork of
-mdBook with the following additional features:
-
-* Add support for hiding lines in other languages
-  [#1339](https://github.com/rust-lang/mdBook/pull/1339)
-* Make `mdbook test` call the `lean` compiler to test the snippets.
-* Ability to test a single chapter at a time which is handy when you
-are working on that chapter.  See the `--chapter` option.
-
-So you need to setup these tools before you can run `mdBook`.
-
-1. install [Rust](https://www.rust-lang.org/tools/install)
-which provides you with the `cargo` tool for building rust packages.
-Then run the following:
-    ```bash
-    cargo install --git https://github.com/leanprover/mdBook mdbook
-    ```
-
-1. Clone https://github.com/leanprover/LeanInk.git and run `lake build` then make the resulting
-   binary available to Alectryon using e.g.
-    ```bash
-    # make `leanInk` available in the current shell
-    export PATH=$PWD/build/bin:$PATH
-    ```
-
-1. Create a Python 3.10 environment.
-
-1. Install Alectryon:
-    ```
-    python3 -m pip install git+https://github.com/Kha/alectryon.git@typeid
-    ```
-
-1. Now you are ready to process the `*.lean` files using Alectryon as follows:
-
-    ```
-    cd lean4/doc
-    alectryon --frontend lean4+markup examples/palindromes.lean --backend webpage -o palindromes.lean.md
-    ```
-
-    Repeat this for the other .lean files you care about or write a script to process them all.
-
-1. Now you can build the book using:
-    ```
-    cd lean4/doc
-    mdbook build
-    ```
-
-This will put the HTML in a `out` folder so you can load `out/index.html` in your web browser and
-it should look like https://leanprover.github.io/lean4/doc/.
-
-1. It is also handy to use e.g. [`mdbook watch`](https://rust-lang.github.io/mdBook/cli/watch.html)
-   in the `doc/` folder so that it keeps the html up to date while you are editing.
-
-    ```bash
-    mdbook watch --open  # opens the output in `out/` in your default browser
-    ```
-
-## Testing Lean Snippets
-
-You can run the following in the `doc/` folder to test all the lean code snippets.
-
-    ```bash
-    mdbook test
-    ```
-
-and you can use the `--chapter` option to test a specific chapter that you are working on:
-
-    ```bash
-    mdbook test --chapter Array
-    ```
-
-Use chapter name `?` to get a list of all the chapter names.

doc/dev/testing.md

@@ -1,121 +0,0 @@
-# Test Suite
-
-After [building Lean](../make/index.md) you can run all the tests using
-```
-cd build/release
-make test ARGS=-j4
-```
-
-Change the 4 to the maximum number of parallel tests you want to
-allow. The best choice is the number of CPU cores on your machine as
-the tests are mostly CPU bound.  You can find the number of processors
-on linux using `nproc` and on Windows it is the `NUMBER_OF_PROCESSORS`
-environment variable.
-
-You can run tests after [building a specific stage](bootstrap.md) by
-adding the `-C stageN` argument. The default when run as above is stage 1.  The
-Lean tests will automatically use that stage's corresponding Lean
-executables
-
-You can also use `ctest` directly if you are in the right folder.  So
-to run stage1 tests with a 300 second timeout run this:
-
-```bash
-cd build/release/stage1
-ctest -j 4 --output-on-failure --timeout 300
-```
-
-To get verbose output from ctest pass the `--verbose` command line
-option. Test output is normally suppressed and only summary
-information is displayed. This option will show all test output.
-
-## Test Suite Organization
-
-All these tests are included by [src/shell/CMakeLists.txt](https://github.com/leanprover/lean4/blob/master/src/shell/CMakeLists.txt):
-
-- `tests/lean`: contains tests that come equipped with a
-  .lean.expected.out file. The driver script `test_single.sh` runs
-  each test and checks the actual output (*.produced.out) with the
-  checked in expected output.
-
-- `tests/lean/run`: contains tests that are run through the lean
-  command line one file at a time. These tests only look for error
-  codes and do not check the expected output even though output is
-  produced, it is ignored.
-
-- `tests/lean/interactive`: are designed to test server requests at a
-  given position in the input file. Each .lean file contains comments
-  that indicate how to simulate a client request at that position.
-  using a `--^` point to the line position. Example:
-    ```lean,ignore
-    open Foo in
-    theorem tst2 (h : a ≤ b) : a + 2 ≤ b + 2 :=
-    Bla.
-      --^ textDocument/completion
-    ```
-    In this example, the test driver `test_single.sh` will simulate an
-    auto-completion request at `Bla.`. The expected output is stored in
-    a .lean.expected.out in the json format that is part of the
-    [Language Server
-    Protocol](https://microsoft.github.io/language-server-protocol/).
-
-    This can also be used to test the following additional requests:
-    ```
-    --^ textDocument/hover
-    --^ textDocument/typeDefinition
-    --^ textDocument/definition
-    --^ $/lean/plainGoal
-    --^ $/lean/plainTermGoal
-    --^ insert: ...
-    --^ collectDiagnostics
-    ```
-
-- `tests/lean/server`: Tests more of the Lean `--server` protocol.
-  There are just a few of them, and it uses .log files containing
-  JSON.
-
-- `tests/compiler`: contains tests that will run the Lean compiler and
-  build an executable that is executed and the output is compared to
-  the .lean.expected.out file. This test also contains a subfolder
-  `foreign` which shows how to extend Lean using C++.
-
-- `tests/lean/trust0`: tests that run Lean in a mode that Lean doesn't
-  even trust the .olean files (i.e., trust 0).
-
-- `tests/bench`: contains performance tests.
-
-- `tests/plugin`: tests that compiled Lean code can be loaded into
-  `lean` via the `--plugin` command line option.
-
-## Fixing Tests
-
-When the Lean source code or the standard library are modified, some of the
-tests break because the produced output is slightly different, and we have
-to reflect the changes in the `.lean.expected.out` files.
-We should not blindly copy the new produced output since we may accidentally
-miss a bug introduced by recent changes.
-The test suite contains commands that allow us to see what changed in a convenient way.
-First, we must install [meld](http://meldmerge.org/). On Ubuntu, we can do it by simply executing
-
-```
-sudo apt-get install meld
-```
-
-Now, suppose `bad_class.lean` test is broken. We can see the problem by going to `test/lean` directory and
-executing
-
-```
-./test_single.sh -i bad_class.lean
-```
-
-When the `-i` option is provided, `meld` is automatically invoked
-whenever there is discrepancy between the produced and expected
-outputs. `meld` can also be used to repair the problems.
-
-In Emacs, we can also execute `M-x lean4-diff-test-file` to check/diff the file of the current buffer.
-To mass-copy all `.produced.out` files to the respective `.expected.out` file, use `tests/lean/copy-produced`.
-When using the Nix setup, add `--keep-failed` to the `nix build` call and then call
-```sh
-tests/lean/copy-produced <build-dir>/source/tests/lean
-```
-instead where `<build-dir>` is the path printed out by `nix build`.

doc/do.md

@@ -276,8 +276,8 @@ def sum (xs : Array Nat) : IO Nat := do
 -- x: 3
 -- 6
 
--- We can write pure code using the `Id.run <| do` DSL too.
-def sum' (xs : Array Nat) : Nat := Id.run <| do
+-- We can write pure code using the `do` DSL too.
+def sum' (xs : Array Nat) : Nat := do
   let mut s := 0
   for x in xs do
     s := s + x
@@ -348,46 +348,6 @@ TODO: describe `forIn`
 
 TODO
 
-## Returning early from a failed match
-
-Inside a `do` block, the pattern `let _ ← <success> | <fail>` will continue with the rest of the block if the match on the left hand side succeeds, but will execute the right hand side and exit the block on failure:
-
-```lean
-def showUserInfo (getUsername getFavoriteColor : IO (Option String)) : IO Unit := do
-  let some n ← getUsername | IO.println "no username!"
-  IO.println s!"username: {n}"
-  let some c ← getFavoriteColor | IO.println "user didn't provide a favorite color!"
-  IO.println s!"favorite color: {c}"
-
--- username: JohnDoe
--- favorite color: red
-#eval showUserInfo (pure <| some "JohnDoe") (pure <| some "red")
-
--- no username
-#eval showUserInfo (pure none) (pure <| some "purple")
-
--- username: JaneDoe
--- user didn't provide a favorite color
-#eval showUserInfo (pure <| some "JaneDoe") (pure none)
-```
-
-## If-let
-
-Inside a `do` block, users can employ the `if let` pattern to destructure actions:
-
-```lean
-def tryIncrement (getInput : IO (Option Nat)) : IO (Except String Nat) := do
-  if let some n ← getInput
-  then return Except.ok n.succ
-  else return Except.error "argument was `none`"
-
--- Except.ok 2
-#eval tryIncrement (pure <| some 1)
-
--- Except.error "argument was `none`"
-#eval tryIncrement (pure <| none)
-```
-
 ## Pattern matching
 
 TODO

doc/elaborators.md

@@ -1,8 +0,0 @@
-## Elaborators
-
-TODO. See [Lean Together 2021: Metaprogramming in Lean
-4](https://youtu.be/hxQ1vvhYN_U) for an overview as well [the
-continuation](https://youtu.be/vy4JWIiiXSY) about tactic programming.
-For more information on antiquotations, see also §4.1 of [Beyond
-Notations: Hygienic Macro Expansion for Theorem Proving
-Languages](https://arxiv.org/pdf/2001.10490.pdf#page=11).

doc/examples.md

@@ -1,9 +0,0 @@
-Examples
-========
-
-- [Palindromes](examples/palindromes.lean.md)
-- [Binary Search Trees](examples/bintree.lean.md)
-- [A Certified Type Checker](examples/tc.lean.md)
-- [The Well-Typed Interpreter](examples/interp.lean.md)
-- [Dependent de Bruijn Indices](examples/deBruijn.lean.md)
-- [Parametric Higher-Order Abstract Syntax](examples/phoas.lean.md)

doc/examples/Certora2022/ex1.lean

@@ -1,22 +0,0 @@
-/- "Hello world" -/
-
-#eval "hello" ++ " " ++ "world"
--- "hello world"
-
-#check true
--- Bool
-
-def x := 10
-
-#eval x + 2
--- 12
-
-def double (x : Int) := 2*x
-
-#eval double 3
--- 6
-#check double
--- Int → Int
-example : double 4 = 8 := rfl
-
-

doc/examples/Certora2022/ex10.lean

@@ -1,19 +0,0 @@
-/- Dependent pattern matching -/
-
-inductive Vector (α : Type u) : Nat → Type u
-  | nil : Vector α 0
-  | cons : α → Vector α n → Vector α (n+1)
-
-infix:67 "::" => Vector.cons
-
-def Vector.zip : Vector α n → Vector β n → Vector (α × β) n
-  | nil, nil => nil
-  | a::as, b::bs => (a, b) :: zip as bs
-
-#print Vector.zip
-/-
-def Vector.zip.{u_1, u_2} : {α : Type u_1} → {n : Nat} → {β : Type u_2} → Vector α n → Vector β n → Vector (α × β) n :=
-fun {α} {n} {β} x x_1 =>
-  Vector.brecOn (motive := fun {n} x => {β : Type u_2} → Vector β n → Vector (α × β) n) x
-    ...
--/

doc/examples/Certora2022/ex11.lean

@@ -1,22 +0,0 @@
-/- Structures -/
-
-structure Point where
-  x : Int := 0
-  y : Int := 0
-  deriving Repr
-
-#eval Point.x (Point.mk 10 20)
--- 10
-
-#eval { x := 10, y := 20 : Point }
-
-def p : Point := { y := 20 }
-
-#eval p.x
-#eval p.y
-#eval { p with x := 5 }
--- { x := 5, y := 20 }
-
-structure Point3D extends Point where
-  z : Int
-

doc/examples/Certora2022/ex12.lean

@@ -1,28 +0,0 @@
-/- Type classes -/
-namespace Example
-
-class ToString (α : Type u) where
-  toString : α → String
-
-#check @ToString.toString
--- {α : Type u_1} → [self : ToString α] → α → String
-
-instance : ToString String where
-  toString s := s
-
-instance : ToString Bool where
-  toString b := if b then "true" else "false"
-
-#eval ToString.toString "hello"
-export ToString (toString)
-#eval toString true
--- "true"
--- #eval toString (true, "hello") -- Error
-
-instance [ToString α] [ToString β] : ToString (α × β) where
-  toString p := "(" ++ toString p.1 ++ ", " ++ toString p.2 ++ ")"
-
-#eval toString (true, "hello")
--- "(true, hello)"
-
-end Example

doc/examples/Certora2022/ex13.lean

@@ -1,44 +0,0 @@
-/- Type classes are heavily used in Lean -/
-namespace Example
-
-class Mul (α : Type u) where
-  mul : α → α → α
-
-infixl:70 " * " => Mul.mul
-
-def double [Mul α] (a : α) := a * a
-
-class Semigroup (α : Type u) extends Mul α where
-  mul_assoc : ∀ a b c : α, (a * b) * c = a * (b * c)
-
-instance : Semigroup Nat where
-  mul := Nat.mul
-  mul_assoc := Nat.mul_assoc
-
-#eval double 5
-
-class Functor (f : Type u → Type v) : Type (max (u+1) v) where
-  map : (α → β) → f α → f β
-
-infixr:100 " <$> " => Functor.map
-
-class LawfulFunctor (f : Type u → Type v) [Functor f] : Prop where
-  id_map   (x : f α) : id <$> x = x
-  comp_map (g : α → β) (h : β → γ) (x : f α) :(h ∘ g) <$> x = h <$> g <$> x
-
-end Example
-
-/-
-`Deriving instances automatically`
-
-We have seen `deriving Repr` in a few examples.
-It is an instance generator.
-Lean comes equipped with generators for the following classes.
-`Repr`, `Inhabited`, `BEq`, `DecidableEq`,
-`Hashable`, `Ord`, `FromToJson`, `SizeOf`
--/
-
-inductive Tree (α : Type u) where
-  | leaf (val : α)
-  | node (left right : Tree α)
-  deriving DecidableEq, Ord, Inhabited, Repr

doc/examples/Certora2022/ex14.lean

@@ -1,31 +0,0 @@
-/- Tactics -/
-
-example : p → q → p ∧ q ∧ p := by
-  intro hp hq
-  apply And.intro
-  exact hp
-  apply And.intro
-  exact hq
-  exact hp
-
-example : p → q → p ∧ q ∧ p := by
-  intro hp hq; apply And.intro hp; exact And.intro hq hp
-
-/- Structuring proofs -/
-
-example : p → q → p ∧ q ∧ p := by
-  intro hp hq
-  apply And.intro
-  case left => exact hp
-  case right =>
-    apply And.intro
-    case left => exact hq
-    case right => exact hp
-
-example : p → q → p ∧ q ∧ p := by
-  intro hp hq
-  apply And.intro
-  . exact hp
-  . apply And.intro
-    . exact hq
-    . exact hp

doc/examples/Certora2022/ex15.lean

@@ -1,19 +0,0 @@
-/- intro tactic variants -/
-
-example (p q : α → Prop) : (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x := by
-  intro h
-  match h with
-  | Exists.intro w (And.intro hp hq) => exact Exists.intro w (And.intro hq hp)
-
-example (p q : α → Prop) : (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x := by
-  intro (Exists.intro _ (And.intro hp hq))
-  exact Exists.intro _ (And.intro hq hp)
-
-example (p q : α → Prop) : (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x := by
-  intro ⟨_, hp, hq⟩
-  exact ⟨_, hq, hp⟩
-
-example (α : Type) (p q : α → Prop) : (∃ x, p x ∨ q x) → ∃ x, q x ∨ p x := by
-  intro
-    | ⟨_, .inl h⟩ => exact ⟨_, .inr h⟩
-    | ⟨_, .inr h⟩ => exact ⟨_, .inl h⟩

doc/examples/Certora2022/ex16.lean

@@ -1,12 +0,0 @@
-/- Inaccessible names -/
-
-example : ∀ x y : Nat, x = y → y = x := by
-  intros
-  apply Eq.symm
-  assumption
-
-example : ∀ x y : Nat, x = y → y = x := by
-  intros
-  apply Eq.symm
-  rename_i a b hab
-  exact hab

doc/examples/Certora2022/ex17.lean

@@ -1,19 +0,0 @@
-/- More tactics -/
-
-example (p q : Nat → Prop) : (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x := by
-  intro h
-  cases h with
-  | intro x hpq =>
-    cases hpq with
-    | intro hp hq =>
-      exists x
-
-example : p ∧ q → q ∧ p := by
-  intro p
-  cases p
-  constructor <;> assumption
-
-example : p ∧ ¬ p → q := by
-  intro h
-  cases h
-  contradiction

doc/examples/Certora2022/ex18.lean

@@ -1,20 +0,0 @@
-/- Structuring proofs (cont.) -/
-
-example : p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r) := by
-  intro h
-  have hp : p := h.left
-  have hqr : q ∨ r := h.right
-  show (p ∧ q) ∨ (p ∧ r)
-  cases hqr with
-  | inl hq => exact Or.inl ⟨hp, hq⟩
-  | inr hr => exact Or.inr ⟨hp, hr⟩
-
-example : p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r) := by
-  intro ⟨hp, hqr⟩
-  cases hqr with
-  | inl hq =>
-    have := And.intro hp hq
-    apply Or.inl; exact this
-  | inr hr =>
-    have := And.intro hp hr
-    apply Or.inr; exact this

doc/examples/Certora2022/ex19.lean

@@ -1,10 +0,0 @@
-/- Tactic combinators -/
-
-example : p → q → r → p ∧ ((p ∧ q) ∧ r) ∧ (q ∧ r ∧ p) := by
-  intros
-  repeat (any_goals constructor)
-  all_goals assumption
-
-example : p → q → r → p ∧ ((p ∧ q) ∧ r) ∧ (q ∧ r ∧ p) := by
-  intros
-  repeat (any_goals (first | assumption | constructor))

doc/examples/Certora2022/ex2.lean

@@ -1,14 +0,0 @@
-/- First-class functions -/
-
-def twice (f : Nat → Nat) (a : Nat) :=
-  f (f a)
-
-#check twice
--- (Nat → Nat) → Nat → Nat
-
-#eval twice (fun x => x + 2) 10
-
-theorem twice_add_2 (a : Nat) : twice (fun x => x + 2) a = a + 4 := rfl
-
--- `(· + 2)` is syntax sugar for `(fun x => x + 2)`.
-#eval twice (· + 2) 10

doc/examples/Certora2022/ex20.lean

@@ -1,22 +0,0 @@
-/- Rewriting -/
-
-example (f : Nat → Nat) (k : Nat) (h₁ : f 0 = 0) (h₂ : k = 0) : f k = 0 := by
-  rw [h₂] -- replace k with 0
-  rw [h₁] -- replace f 0 with 0
-
-example (f : Nat → Nat) (k : Nat) (h₁ : f 0 = 0) (h₂ : k = 0) : f k = 0 := by
-  rw [h₂, h₁]
-
-example (f : Nat → Nat) (a b : Nat) (h₁ : a = b) (h₂ : f a = 0) : f b = 0 := by
-  rw [← h₁, h₂]
-
-example (f : Nat → Nat) (a : Nat) (h : 0 + a = 0) : f a = f 0 := by
-  rw [Nat.zero_add] at h
-  rw [h]
-
-def Tuple (α : Type) (n : Nat) :=
-  { as : List α // as.length = n }
-
-example (n : Nat) (h : n = 0) (t : Tuple α n) : Tuple α 0 := by
-  rw [h] at t
-  exact t

doc/examples/Certora2022/ex21.lean

@@ -1,21 +0,0 @@
-/- Simplifier -/
-
-example (p : Nat → Prop) : (x + 0) * (0 + y * 1 + z * 0) = x * y := by
-  simp
-
-example (p : Nat → Prop) (h : p (x * y)) : p ((x + 0) * (0 + y * 1 + z * 0)) := by
-  simp; assumption
-
-example (p : Nat → Prop) (h : p ((x + 0) * (0 + y * 1 + z * 0))) : p (x * y) := by
-  simp at h; assumption
-
-def f (m n : Nat) : Nat :=
-  m + n + m
-
-example (h : n = 1) (h' : 0 = m) : (f m n) = n := by
-  simp [h, ←h', f]
-
-example (p : Nat → Prop) (h₁ : x + 0 = x') (h₂ : y + 0 = y')
-        : x + y + 0 = x' + y' := by
-  simp at *
-  simp [*]

doc/examples/Certora2022/ex22.lean

@@ -1,13 +0,0 @@
-/- Simplifier -/
-
-def mk_symm (xs : List α) :=
-  xs ++ xs.reverse
-
-@[simp] theorem reverse_mk_symm : (mk_symm xs).reverse = mk_symm xs := by
-  simp [mk_symm]
-
-theorem tst : (xs ++ mk_symm ys).reverse = mk_symm ys ++ xs.reverse := by
-  simp
-
-#print tst
--- Lean reverse_mk_symm, and List.reverse_append

doc/examples/Certora2022/ex23.lean

@@ -1,26 +0,0 @@
-/- split tactic -/
-
-def f (x y z : Nat) : Nat :=
-  match x, y, z with
-  | 5, _, _ => y
-  | _, 5, _ => y
-  | _, _, 5 => y
-  | _, _, _ => 1
-
-example : x ≠ 5 → y ≠ 5 → z ≠ 5 → z = w → f x y w = 1 := by
-  intros
-  simp [f]
-  split
-  . contradiction
-  . contradiction
-  . contradiction
-  . rfl
-
-def g (xs ys : List Nat) : Nat :=
-  match xs, ys with
-  | [a, b], _ => a+b+1
-  | _, [b, c] => b+1
-  | _, _      => 1
-
-example (xs ys : List Nat) (h : g xs ys = 0) : False := by
-  unfold g at h; split at h <;> simp_arith at h

doc/examples/Certora2022/ex24.lean

@@ -1,9 +0,0 @@
-/- induction tactic -/
-
-example (as : List α) (a : α) : (as.concat a).length = as.length + 1 := by
-  induction as with
-  | nil => rfl
-  | cons _ xs ih => simp [List.concat, ih]
-
-example (as : List α) (a : α) : (as.concat a).length = as.length + 1 := by
-  induction as <;> simp! [*]

doc/examples/Certora2022/ex3.lean

@@ -1,59 +0,0 @@
-/- Enumerated types -/
-
-inductive Weekday where
-  | sunday | monday | tuesday | wednesday
-  | thursday | friday | saturday
-
-#check Weekday.sunday
--- Weekday
-
-open Weekday
-#check sunday
-
-def natOfWeekday (d : Weekday) : Nat :=
-  match d with
-  | sunday    => 1
-  | monday    => 2
-  | tuesday   => 3
-  | wednesday => 4
-  | thursday  => 5
-  | friday    => 6
-  | saturday  => 7
-
-def Weekday.next (d : Weekday) : Weekday :=
-  match d with
-  | sunday    => monday
-  | monday    => tuesday
-  | tuesday   => wednesday
-  | wednesday => thursday
-  | thursday  => friday
-  | friday    => saturday
-  | saturday  => sunday
-
-def Weekday.previous : Weekday → Weekday
-  | sunday    => saturday
-  | monday    => sunday
-  | tuesday   => monday
-  | wednesday => tuesday
-  | thursday  => wednesday
-  | friday    => thursday
-  | saturday  => friday
-
-/- Proving theorems using tactics -/
-
-theorem Weekday.next_previous (d : Weekday) : d.next.previous = d :=
-  match d with
-  | sunday    => rfl
-  | monday    => rfl
-  | tuesday   => rfl
-  | wednesday => rfl
-  | thursday  => rfl
-  | friday    => rfl
-  | saturday  => rfl
-
-theorem Weekday.next_previous' (d : Weekday) : d.next.previous = d := by -- switch to tactic mode
-  cases d -- Creates 7 goals
-  rfl; rfl; rfl; rfl; rfl; rfl; rfl
-
-theorem Weekday.next_previous'' (d : Weekday) : d.next.previous = d := by
-  cases d <;> rfl

doc/examples/Certora2022/ex4.lean

@@ -1,20 +0,0 @@
-/- What is the type of Nat? -/
-
-#check 0
--- Nat
-#check Nat
--- Type
-#check Type
--- Type 1
-#check Type 1
--- Type 2
-#check Eq.refl 2
--- 2 = 2
-#check 2 = 2
--- Prop
-#check Prop
--- Type
-
-example : Prop = Sort 0   := rfl
-example : Type = Sort 1   := rfl
-example : Type 1 = Sort 2 := rfl

doc/examples/Certora2022/ex5.lean

@@ -1,21 +0,0 @@
-/- Implicit arguments and universe polymorphism -/
-
-def f (α β : Sort u) (a : α) (b : β) : α := a
-
-#eval f Nat String 1 "hello"
--- 1
-
-def g {α β : Sort u} (a : α) (b : β) : α := a
-
-#eval g 1 "hello"
-
-def h (a : α) (b : β) : α := a
-
-#check g
--- ?m.1 → ?m.2 → ?m.1
-#check @g
--- {α β : Sort u} → α → β → α
-#check @h
--- {α : Sort u_1} → {β : Sort u_2} → α → β → α
-#check g (α := Nat) (β := String)
--- Nat → String → Nat

doc/examples/Certora2022/ex6.lean

@@ -1,14 +0,0 @@
-/- Inductive Types -/
-
-inductive Tree (β : Type v) where
-  | leaf
-  | node (left : Tree β) (key : Nat) (value : β) (right : Tree β)
-  deriving Repr
-
-#eval Tree.node .leaf 10 true .leaf
--- Tree.node Tree.leaf 10 true Tree.leaf
-
-inductive Vector (α : Type u) : Nat → Type u
-  | nil : Vector α 0
-  | cons : α → Vector α n → Vector α (n+1)
-

doc/examples/Certora2022/ex7.lean

@@ -1,25 +0,0 @@
-/- Recursive functions -/
-
-#print Nat -- Nat is an inductive datatype
-
-def fib (n : Nat) : Nat :=
-  match n with
-  | 0 => 1
-  | 1 => 1
-  | n+2 => fib (n+1) + fib n
-
-example : fib 5 = 8 := rfl
-
-example : fib (n+2) = fib (n+1) + fib n := rfl
-
-#print fib
-/-
-def fib : Nat → Nat :=
-fun n =>
-  Nat.brecOn n fun n f =>
-    (match (motive := (n : Nat) → Nat.below n → Nat) n with
-      | 0 => fun x => 1
-      | 1 => fun x => 1
-      | Nat.succ (Nat.succ n) => fun x => x.fst.fst + x.fst.snd.fst.fst)
-      f
--/

doc/examples/Certora2022/ex8.lean

@@ -1,25 +0,0 @@
-/- Well-founded recursion -/
-
-def ack : Nat → Nat → Nat
-  | 0,   y   => y+1
-  | x+1, 0   => ack x 1
-  | x+1, y+1 => ack x (ack (x+1) y)
-termination_by ack x y => (x, y)
-
-def sum (a : Array Int) : Int :=
-  let rec go (i : Nat) :=
-     if i < a.size then
-        a[i] + go (i+1)
-     else
-        0
-  go 0
-termination_by go i => a.size - i
-
-set_option pp.proofs true
-#print sum.go
-/-
-def sum.go : Array Int → Nat → Int :=
-fun a =>
-  WellFounded.fix (sum.go.proof_1 a) fun i a_1 =>
-    if h : i < Array.size a then Array.getOp a i + a_1 (i + 1) (sum.go.proof_2 a i h) else 0
--/

doc/examples/Certora2022/ex9.lean

@@ -1,44 +0,0 @@
-/- Mutual recursion -/
-
-inductive Term where
- | const : String → Term
- | app   : String → List Term → Term
-
-namespace Term
-mutual
- def numConsts : Term → Nat
-   | const _ => 1
-   | app _ cs => numConstsLst cs
-
- def numConstsLst : List Term → Nat
-   | [] => 0
-   | c :: cs => numConsts c + numConstsLst cs
-end
-
-mutual
-  def replaceConst (a b : String) : Term → Term
-   | const c => if a = c then const b else const c
-   | app f cs => app f (replaceConstLst a b cs)
-
-  def replaceConstLst (a b : String) : List Term → List Term
-   | [] => []
-   | c :: cs => replaceConst a b c :: replaceConstLst a b cs
-end
-
-/- Mutual recursion in theorems -/
-
-mutual
-  theorem numConsts_replaceConst (a b : String) (e : Term)
-            : numConsts (replaceConst a b e) = numConsts e := by
-    match e with
-    | const c => simp [replaceConst]; split <;> simp [numConsts]
-    | app f cs => simp [replaceConst, numConsts, numConsts_replaceConstLst a b cs]
-
-  theorem numConsts_replaceConstLst (a b : String) (es : List Term)
-            : numConstsLst (replaceConstLst a b es) = numConstsLst es := by
-    match es with
-    | [] => simp [replaceConstLst, numConstsLst]
-    | c :: cs =>
-      simp [replaceConstLst, numConstsLst, numConsts_replaceConst a b c,
-            numConsts_replaceConstLst a b cs]
-end

doc/examples/ICERM2022/ctor.lean

@@ -1,46 +0,0 @@
-import Lean
-
-open Lean Meta
-
-def ctor (mvarId : MVarId) (idx : Nat) : MetaM (List MVarId) := do
-  /- Set `MetaM` context using `mvarId` -/
-  withMVarContext mvarId do 
-    /- Fail if the metavariable is already assigned. -/
-    checkNotAssigned mvarId `ctor
-    /- Retrieve the target type, instantiateMVars, and use `whnf`. -/
-    let target ← getMVarType' mvarId
-    let .const declName us := target.getAppFn
-      | throwTacticEx `ctor mvarId "target is not an inductive datatype"
-    let .inductInfo { ctors, .. } ← getConstInfo declName
-      | throwTacticEx `ctor mvarId "target is not an inductive datatype"
-    if idx = 0 then
-      throwTacticEx `ctor mvarId "invalid index, it must be > 0"  
-    else if h : idx - 1 < ctors.length then
-      apply mvarId (.const ctors[idx - 1] us)
-    else
-      throwTacticEx `ctor mvarId "invalid index, inductive datatype has only {ctors.length} contructors"  
-
-open Elab Tactic
-
-elab "ctor" idx:num : tactic => 
-  liftMetaTactic (ctor · idx.getNat)
-
-example (p : Prop) : p := by 
-  ctor 1 -- Error
-
-example (h : q) : p ∨ q := by 
-  ctor 0 -- Error
-  exact h
-
-example (h : q) : p ∨ q := by 
-  ctor 3 -- Error
-  exact h
-
-example (h : q) : p ∨ q := by 
-  ctor 2
-  exact h
-
-example (h : q) : p ∨ q := by 
-  ctor 1
-  exact h -- Error 
-

doc/examples/ICERM2022/meta.lean

@@ -1,80 +0,0 @@
-import Lean
-
-open Lean Meta
-
-def ex1 (declName : Name) : MetaM Unit := do
-  let info ← getConstInfo declName
-  IO.println s!"{declName} : {← ppExpr info.type}"
-  if let some val := info.value? then 
-    IO.println s!"{declName} : {← ppExpr val}"
-    
-#eval ex1 ``Nat
-
-def ex2 (declName : Name) : MetaM Unit := do
-  let info ← getConstInfo declName
-  trace[Meta.debug] "{declName} : {info.type}"
-  if let some val := info.value? then 
-    trace[Meta.debug] "{declName} : {val}"
-
-#eval ex2 ``Add.add
-
-set_option trace.Meta.debug true in
-#eval ex2 ``Add.add
-
-def ex3 (declName : Name) : MetaM Unit := do
-  let info ← getConstInfo declName
-  forallTelescope info.type fun xs type => do
-    trace[Meta.debug] "hypotheses : {xs}"
-    trace[Meta.debug] "resultType : {type}"
-    for x in xs do
-      trace[Meta.debug] "{x} : {← inferType x}"
-
-def myMin [LT α] [DecidableRel (α := α) (·<·)] (a b : α) : α :=
-  if a < b then 
-    a
-  else 
-    b
-
-set_option trace.Meta.debug true in
-#eval ex3 ``myMin
-
-def ex4 : MetaM Unit := do
-  let nat := mkConst ``Nat
-  withLocalDeclD `a nat fun a => 
-  withLocalDeclD `b nat fun b => do
-    let e ← mkAppM ``HAdd.hAdd #[a, b]
-    trace[Meta.debug] "{e} : {← inferType e}"
-    let e ← mkAdd a (mkNatLit 5)
-    trace[Meta.debug] "added 5: {e}"
-    let e ← whnf e
-    trace[Meta.debug] "whnf: {e}"
-    let e ← reduce e
-    trace[Meta.debug] "reduced: {e}"
-    let a_plus_1 ← mkAdd a (mkNatLit 1)
-    let succ_a   := mkApp (mkConst ``Nat.succ) a
-    trace[Meta.debug] "({a_plus_1} =?= {succ_a}) == {← isDefEq a_plus_1 succ_a}"
-    let m ← mkFreshExprMVar nat
-    let m_plus_1 ← mkAdd m (mkNatLit 1)
-    trace[Meta.debug] "m_plus_1: {m_plus_1}"
-    unless (← isDefEq m_plus_1 succ_a) do throwError "isDefEq failed"
-    trace[Meta.debug] "m_plus_1: {m_plus_1}"
-
-set_option trace.Meta.debug true in
-#eval ex4
-
-open Elab Term
-
-def ex5 : TermElabM Unit := do
-  let nat := Lean.mkConst ``Nat
-  withLocalDeclD `a nat fun a => do 
-  withLocalDeclD `b nat fun b => do
-    let ab ← mkAppM ``HAdd.hAdd #[a, b]
-    let stx ← `(fun x => if x < 10 then $(← exprToSyntax ab) + x else x + $(← exprToSyntax a))
-    let e ← elabTerm stx none
-    trace[Meta.debug] "{e} : {← inferType e}"
-    let e := mkApp e (mkNatLit 5)
-    let e ← whnf e
-    trace[Meta.debug] "{e}"
-       
-set_option trace.Meta.debug true in
-#eval ex5

doc/examples/ICERM2022/notation.lean

@@ -1,49 +0,0 @@
-import Lean
-
-def f (x y : Nat) := x * y + 1
-
-infixl:65 " *' " => f
-
-#check 2 *' 3
-
-notation "unitTest " x => Prod.mk x ()
-
-#check unitTest 42
-
-notation "parenthesisTest " x => Nat.sub (x)
-#check parenthesisTest 12
-
-def Set (α : Type u) := α → Prop
-def setOf {α : Type} (p : α → Prop) : Set α := p
-notation "{ " x " | " p " }" => setOf (fun x => p)
-
-#check { x | x ≤ 1 }
-
-notation "cdotTest " "(" x ", " y ")" => Prod.map (· + 1) (1 + ·) (x, y)
-
-#check cdotTest (13, 12)
-
-notation "tupleFunctionTest " "(" x ", " y ")"=> Prod.map (Nat.add 1) (Nat.add 2) (x, y)
-
-#check tupleFunctionTest (15, 12)
-
-notation "diag " x => Prod.mk x x
-
-#check diag 12
-
-open Lean Meta PrettyPrinter Delaborator SubExpr in
-@[delab app.Prod.mk] def delabDoubleRhsTest : Delab := do
-   let e ← getExpr
-   let #[_, _, x, y] := e.getAppArgs | failure
-   guard (← isDefEq x y) 
-   let stx ← withAppArg delab
-   `(diag $stx)     
-
-#check diag 3
-#check (3, 3)
-#check (3, 4)
-#check (2+1, 3)
-#check (true, true)
-
-
-

doc/examples/NFM2022/nfm1.lean

@@ -1,22 +0,0 @@
-/- "Hello world" -/
-
-#eval "hello" ++ " " ++ "world"
--- "hello world"
-
-#check true
--- Bool
-
-def x := 10
-
-#eval x + 2
--- 12
-
-def double (x : Int) := 2*x
-
-#eval double 3
--- 6
-#check double
--- Int → Int
-example : double 4 = 8 := rfl
-
-

doc/examples/NFM2022/nfm10.lean

@@ -1,19 +0,0 @@
-/- Dependent pattern matching -/
-
-inductive Vector (α : Type u) : Nat → Type u
-  | nil : Vector α 0
-  | cons : α → Vector α n → Vector α (n+1)
-
-infix:67 "::" => Vector.cons
-
-def Vector.zip : Vector α n → Vector β n → Vector (α × β) n
-  | nil, nil => nil
-  | a::as, b::bs => (a, b) :: zip as bs
-
-#print Vector.zip
-/-
-def Vector.zip.{u_1, u_2} : {α : Type u_1} → {n : Nat} → {β : Type u_2} → Vector α n → Vector β n → Vector (α × β) n :=
-fun {α} {n} {β} x x_1 =>
-  Vector.brecOn (motive := fun {n} x => {β : Type u_2} → Vector β n → Vector (α × β) n) x
-    ...
--/

doc/examples/NFM2022/nfm11.lean

@@ -1,22 +0,0 @@
-/- Structures -/
-
-structure Point where
-  x : Int := 0
-  y : Int := 0
-  deriving Repr
-
-#eval Point.x (Point.mk 10 20)
--- 10
-
-#eval { x := 10, y := 20 : Point }
-
-def p : Point := { y := 20 }
-
-#eval p.x
-#eval p.y
-#eval { p with x := 5 }
--- { x := 5, y := 20 }
-
-structure Point3D extends Point where
-  z : Int
-

doc/examples/NFM2022/nfm12.lean

@@ -1,28 +0,0 @@
-/- Type classes -/
-namespace Example
-
-class ToString (α : Type u) where
-  toString : α → String
-
-#check @ToString.toString
--- {α : Type u_1} → [self : ToString α] → α → String
-
-instance : ToString String where
-  toString s := s
-
-instance : ToString Bool where
-  toString b := if b then "true" else "false"
-
-#eval ToString.toString "hello"
-export ToString (toString)
-#eval toString true
--- "true"
--- #eval toString (true, "hello") -- Error
-
-instance [ToString α] [ToString β] : ToString (α × β) where
-  toString p := "(" ++ toString p.1 ++ ", " ++ toString p.2 ++ ")"
-
-#eval toString (true, "hello")
--- "(true, hello)"
-
-end Example

doc/examples/NFM2022/nfm13.lean

@@ -1,44 +0,0 @@
-/- Type classes are heavily used in Lean -/
-namespace Example
-
-class Mul (α : Type u) where
-  mul : α → α → α
-
-infixl:70 " * " => Mul.mul
-
-def double [Mul α] (a : α) := a * a
-
-class Semigroup (α : Type u) extends Mul α where
-  mul_assoc : ∀ a b c : α, (a * b) * c = a * (b * c)
-
-instance : Semigroup Nat where
-  mul := Nat.mul
-  mul_assoc := Nat.mul_assoc
-
-#eval double 5
-
-class Functor (f : Type u → Type v) : Type (max (u+1) v) where
-  map : (α → β) → f α → f β
-
-infixr:100 " <$> " => Functor.map
-
-class LawfulFunctor (f : Type u → Type v) [Functor f] : Prop where
-  id_map   (x : f α) : id <$> x = x
-  comp_map (g : α → β) (h : β → γ) (x : f α) :(h ∘ g) <$> x = h <$> g <$> x
-
-end Example
-
-/-
-`Deriving instances automatically`
-
-We have seen `deriving Repr` in a few examples.
-It is an instance generator.
-Lean comes equipped with generators for the following classes.
-`Repr`, `Inhabited`, `BEq`, `DecidableEq`,
-`Hashable`, `Ord`, `FromToJson`, `SizeOf`
--/
-
-inductive Tree (α : Type u) where
-  | leaf (val : α)
-  | node (left right : Tree α)
-  deriving DecidableEq, Ord, Inhabited, Repr

doc/examples/NFM2022/nfm14.lean

@@ -1,31 +0,0 @@
-/- Tactics -/
-
-example : p → q → p ∧ q ∧ p := by
-  intro hp hq
-  apply And.intro
-  exact hp
-  apply And.intro
-  exact hq
-  exact hp
-
-example : p → q → p ∧ q ∧ p := by
-  intro hp hq; apply And.intro hp; exact And.intro hq hp
-
-/- Structuring proofs -/
-
-example : p → q → p ∧ q ∧ p := by
-  intro hp hq
-  apply And.intro
-  case left => exact hp
-  case right =>
-    apply And.intro
-    case left => exact hq
-    case right => exact hp
-
-example : p → q → p ∧ q ∧ p := by
-  intro hp hq
-  apply And.intro
-  . exact hp
-  . apply And.intro
-    . exact hq
-    . exact hp

doc/examples/NFM2022/nfm15.lean

@@ -1,19 +0,0 @@
-/- intro tactic variants -/
-
-example (p q : α → Prop) : (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x := by
-  intro h
-  match h with
-  | Exists.intro w (And.intro hp hq) => exact Exists.intro w (And.intro hq hp)
-
-example (p q : α → Prop) : (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x := by
-  intro (Exists.intro _ (And.intro hp hq))
-  exact Exists.intro _ (And.intro hq hp)
-
-example (p q : α → Prop) : (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x := by
-  intro ⟨_, hp, hq⟩
-  exact ⟨_, hq, hp⟩
-
-example (α : Type) (p q : α → Prop) : (∃ x, p x ∨ q x) → ∃ x, q x ∨ p x := by
-  intro
-    | ⟨_, .inl h⟩ => exact ⟨_, .inr h⟩
-    | ⟨_, .inr h⟩ => exact ⟨_, .inl h⟩

doc/examples/NFM2022/nfm16.lean

@@ -1,12 +0,0 @@
-/- Inaccessible names -/
-
-example : ∀ x y : Nat, x = y → y = x := by
-  intros
-  apply Eq.symm
-  assumption
-
-example : ∀ x y : Nat, x = y → y = x := by
-  intros
-  apply Eq.symm
-  rename_i a b hab
-  exact hab

doc/examples/NFM2022/nfm17.lean

@@ -1,19 +0,0 @@
-/- More tactics -/
-
-example (p q : Nat → Prop) : (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x := by
-  intro h
-  cases h with
-  | intro x hpq =>
-    cases hpq with
-    | intro hp hq =>
-      exists x
-
-example : p ∧ q → q ∧ p := by
-  intro p
-  cases p
-  constructor <;> assumption
-
-example : p ∧ ¬ p → q := by
-  intro h
-  cases h
-  contradiction

doc/examples/NFM2022/nfm18.lean

@@ -1,20 +0,0 @@
-/- Structuring proofs (cont.) -/
-
-example : p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r) := by
-  intro h
-  have hp : p := h.left
-  have hqr : q ∨ r := h.right
-  show (p ∧ q) ∨ (p ∧ r)
-  cases hqr with
-  | inl hq => exact Or.inl ⟨hp, hq⟩
-  | inr hr => exact Or.inr ⟨hp, hr⟩
-
-example : p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r) := by
-  intro ⟨hp, hqr⟩
-  cases hqr with
-  | inl hq =>
-    have := And.intro hp hq
-    apply Or.inl; exact this
-  | inr hr =>
-    have := And.intro hp hr
-    apply Or.inr; exact this

doc/examples/NFM2022/nfm19.lean

@@ -1,10 +0,0 @@
-/- Tactic combinators -/
-
-example : p → q → r → p ∧ ((p ∧ q) ∧ r) ∧ (q ∧ r ∧ p) := by
-  intros
-  repeat (any_goals constructor)
-  all_goals assumption
-
-example : p → q → r → p ∧ ((p ∧ q) ∧ r) ∧ (q ∧ r ∧ p) := by
-  intros
-  repeat (any_goals (first | assumption | constructor))

doc/examples/NFM2022/nfm2.lean

@@ -1,14 +0,0 @@
-/- First-class functions -/
-
-def twice (f : Nat → Nat) (a : Nat) :=
-  f (f a)
-
-#check twice
--- (Nat → Nat) → Nat → Nat
-
-#eval twice (fun x => x + 2) 10
-
-theorem twice_add_2 (a : Nat) : twice (fun x => x + 2) a = a + 4 := rfl
-
--- `(· + 2)` is syntax sugar for `(fun x => x + 2)`.
-#eval twice (· + 2) 10

doc/examples/NFM2022/nfm20.lean

@@ -1,22 +0,0 @@
-/- Rewriting -/
-
-example (f : Nat → Nat) (k : Nat) (h₁ : f 0 = 0) (h₂ : k = 0) : f k = 0 := by
-  rw [h₂] -- replace k with 0
-  rw [h₁] -- replace f 0 with 0
-
-example (f : Nat → Nat) (k : Nat) (h₁ : f 0 = 0) (h₂ : k = 0) : f k = 0 := by
-  rw [h₂, h₁]
-
-example (f : Nat → Nat) (a b : Nat) (h₁ : a = b) (h₂ : f a = 0) : f b = 0 := by
-  rw [← h₁, h₂]
-
-example (f : Nat → Nat) (a : Nat) (h : 0 + a = 0) : f a = f 0 := by
-  rw [Nat.zero_add] at h
-  rw [h]
-
-def Tuple (α : Type) (n : Nat) :=
-  { as : List α // as.length = n }
-
-example (n : Nat) (h : n = 0) (t : Tuple α n) : Tuple α 0 := by
-  rw [h] at t
-  exact t

doc/examples/NFM2022/nfm21.lean

@@ -1,21 +0,0 @@
-/- Simplifier -/
-
-example (p : Nat → Prop) : (x + 0) * (0 + y * 1 + z * 0) = x * y := by
-  simp
-
-example (p : Nat → Prop) (h : p (x * y)) : p ((x + 0) * (0 + y * 1 + z * 0)) := by
-  simp; assumption
-
-example (p : Nat → Prop) (h : p ((x + 0) * (0 + y * 1 + z * 0))) : p (x * y) := by
-  simp at h; assumption
-
-def f (m n : Nat) : Nat :=
-  m + n + m
-
-example (h : n = 1) (h' : 0 = m) : (f m n) = n := by
-  simp [h, ←h', f]
-
-example (p : Nat → Prop) (h₁ : x + 0 = x') (h₂ : y + 0 = y')
-        : x + y + 0 = x' + y' := by
-  simp at *
-  simp [*]

doc/examples/NFM2022/nfm22.lean

@@ -1,13 +0,0 @@
-/- Simplifier -/
-
-def mk_symm (xs : List α) :=
-  xs ++ xs.reverse
-
-@[simp] theorem reverse_mk_symm : (mk_symm xs).reverse = mk_symm xs := by
-  simp [mk_symm]
-
-theorem tst : (xs ++ mk_symm ys).reverse = mk_symm ys ++ xs.reverse := by
-  simp
-
-#print tst
--- Lean reverse_mk_symm, and List.reverse_append

doc/examples/NFM2022/nfm23.lean

@@ -1,26 +0,0 @@
-/- split tactic -/
-
-def f (x y z : Nat) : Nat :=
-  match x, y, z with
-  | 5, _, _ => y
-  | _, 5, _ => y
-  | _, _, 5 => y
-  | _, _, _ => 1
-
-example : x ≠ 5 → y ≠ 5 → z ≠ 5 → z = w → f x y w = 1 := by
-  intros
-  simp [f]
-  split
-  . contradiction
-  . contradiction
-  . contradiction
-  . rfl
-
-def g (xs ys : List Nat) : Nat :=
-  match xs, ys with
-  | [a, b], _ => a+b+1
-  | _, [b, c] => b+1
-  | _, _      => 1
-
-example (xs ys : List Nat) (h : g xs ys = 0) : False := by
-  unfold g at h; split at h <;> simp_arith at h

doc/examples/NFM2022/nfm24.lean

@@ -1,9 +0,0 @@
-/- induction tactic -/
-
-example (as : List α) (a : α) : (as.concat a).length = as.length + 1 := by
-  induction as with
-  | nil => rfl
-  | cons x xs ih => simp [List.concat, ih]
-
-example (as : List α) (a : α) : (as.concat a).length = as.length + 1 := by
-  induction as <;> simp! [*]

doc/examples/NFM2022/nfm3.lean

@@ -1,59 +0,0 @@
-/- Enumerated types -/
-
-inductive Weekday where
-  | sunday | monday | tuesday | wednesday
-  | thursday | friday | saturday
-
-#check Weekday.sunday
--- Weekday
-
-open Weekday
-#check sunday
-
-def natOfWeekday (d : Weekday) : Nat :=
-  match d with
-  | sunday    => 1
-  | monday    => 2
-  | tuesday   => 3
-  | wednesday => 4
-  | thursday  => 5
-  | friday    => 6
-  | saturday  => 7
-
-def Weekday.next (d : Weekday) : Weekday :=
-  match d with
-  | sunday    => monday
-  | monday    => tuesday
-  | tuesday   => wednesday
-  | wednesday => thursday
-  | thursday  => friday
-  | friday    => saturday
-  | saturday  => sunday
-
-def Weekday.previous : Weekday → Weekday
-  | sunday    => saturday
-  | monday    => sunday
-  | tuesday   => monday
-  | wednesday => tuesday
-  | thursday  => wednesday
-  | friday    => thursday
-  | saturday  => friday
-
-/- Proving theorems using tactics -/
-
-theorem Weekday.next_previous (d : Weekday) : d.next.previous = d :=
-  match d with
-  | sunday    => rfl
-  | monday    => rfl
-  | tuesday   => rfl
-  | wednesday => rfl
-  | thursday  => rfl
-  | friday    => rfl
-  | saturday  => rfl
-
-theorem Weekday.next_previous' (d : Weekday) : d.next.previous = d := by -- switch to tactic mode
-  cases d -- Creates 7 goals
-  rfl; rfl; rfl; rfl; rfl; rfl; rfl
-
-theorem Weekday.next_previous'' (d : Weekday) : d.next.previous = d := by
-  cases d <;> rfl

doc/examples/NFM2022/nfm4.lean

@@ -1,20 +0,0 @@
-/- What is the type of Nat? -/
-
-#check 0
--- Nat
-#check Nat
--- Type
-#check Type
--- Type 1
-#check Type 1
--- Type 2
-#check Eq.refl 2
--- 2 = 2
-#check 2 = 2
--- Prop
-#check Prop
--- Type
-
-example : Prop = Sort 0   := rfl
-example : Type = Sort 1   := rfl
-example : Type 1 = Sort 2 := rfl

doc/examples/NFM2022/nfm5.lean

@@ -1,21 +0,0 @@
-/- Implicit arguments and universe polymorphism -/
-
-def f (α β : Sort u) (a : α) (b : β) : α := a
-
-#eval f Nat String 1 "hello"
--- 1
-
-def g {α β : Sort u} (a : α) (b : β) : α := a
-
-#eval g 1 "hello"
-
-def h (a : α) (b : β) : α := a
-
-#check g
--- ?m.1 → ?m.2 → ?m.1
-#check @g
--- {α β : Sort u} → α → β → α
-#check @h
--- {α : Sort u_1} → {β : Sort u_2} → α → β → α
-#check g (α := Nat) (β := String)
--- Nat → String → Nat

doc/examples/NFM2022/nfm6.lean

@@ -1,14 +0,0 @@
-/- Inductive Types -/
-
-inductive Tree (β : Type v) where
-  | leaf
-  | node (left : Tree β) (key : Nat) (value : β) (right : Tree β)
-  deriving Repr
-
-#eval Tree.node .leaf 10 true .leaf
--- Tree.node Tree.leaf 10 true Tree.leaf
-
-inductive Vector (α : Type u) : Nat → Type u
-  | nil : Vector α 0
-  | cons : α → Vector α n → Vector α (n+1)
-

doc/examples/NFM2022/nfm7.lean

@@ -1,25 +0,0 @@
-/- Recursive functions -/
-
-#print Nat -- Nat is an inductive datatype
-
-def fib (n : Nat) : Nat :=
-  match n with
-  | 0 => 1
-  | 1 => 1
-  | n+2 => fib (n+1) + fib n
-
-example : fib 5 = 8 := rfl
-
-example : fib (n+2) = fib (n+1) + fib n := rfl
-
-#print fib
-/-
-def fib : Nat → Nat :=
-fun n =>
-  Nat.brecOn n fun n f =>
-    (match (motive := (n : Nat) → Nat.below n → Nat) n with
-      | 0 => fun x => 1
-      | 1 => fun x => 1
-      | Nat.succ (Nat.succ n) => fun x => x.fst.fst + x.fst.snd.fst.fst)
-      f
--/

doc/examples/NFM2022/nfm8.lean

@@ -1,25 +0,0 @@
-/- Well-founded recursion -/
-
-def ack : Nat → Nat → Nat
-  | 0,   y   => y+1
-  | x+1, 0   => ack x 1
-  | x+1, y+1 => ack x (ack (x+1) y)
-termination_by ack x y => (x, y)
-
-def sum (a : Array Int) : Int :=
-  let rec go (i : Nat) :=
-     if i < a.size then
-        a[i] + go (i+1)
-     else
-        0
-  go 0
-termination_by go i => a.size - i
-
-set_option pp.proofs true
-#print sum.go
-/-
-def sum.go : Array Int → Nat → Int :=
-fun a =>
-  WellFounded.fix (sum.go.proof_1 a) fun i a_1 =>
-    if h : i < Array.size a then Array.getOp a i + a_1 (i + 1) (sum.go.proof_2 a i h) else 0
--/

doc/examples/NFM2022/nfm9.lean

@@ -1,44 +0,0 @@
-/- Mutual recursion -/
-
-inductive Term where
- | const : String → Term
- | app   : String → List Term → Term
-
-namespace Term
-mutual
- def numConsts : Term → Nat
-   | const _ => 1
-   | app _ cs => numConstsLst cs
-
- def numConstsLst : List Term → Nat
-   | [] => 0
-   | c :: cs => numConsts c + numConstsLst cs
-end
-
-mutual
-  def replaceConst (a b : String) : Term → Term
-   | const c => if a = c then const b else const c
-   | app f cs => app f (replaceConstLst a b cs)
-
-  def replaceConstLst (a b : String) : List Term → List Term
-   | [] => []
-   | c :: cs => replaceConst a b c :: replaceConstLst a b cs
-end
-
-/- Mutual recursion in theorems -/
-
-mutual
-  theorem numConsts_replaceConst (a b : String) (e : Term)
-            : numConsts (replaceConst a b e) = numConsts e := by
-    match e with
-    | const c => simp [replaceConst]; split <;> simp [numConsts]
-    | app f cs => simp [replaceConst, numConsts, numConsts_replaceConstLst a b cs]
-
-  theorem numConsts_replaceConstLst (a b : String) (es : List Term)
-            : numConstsLst (replaceConstLst a b es) = numConstsLst es := by
-    match es with
-    | [] => simp [replaceConstLst, numConstsLst]
-    | c :: cs =>
-      simp [replaceConstLst, numConstsLst, numConsts_replaceConst a b c,
-            numConsts_replaceConstLst a b cs]
-end

doc/examples/bintree.lean

@@ -1,296 +0,0 @@
-/-!
-# Binary Search Trees
-
-If the type of keys can be totally ordered -- that is, it supports a well-behaved `≤` comparison --
-then maps can be implemented with binary search trees (BSTs). Insert and lookup operations on BSTs take time
-proportional to the height of the tree. If the tree is balanced, the operations therefore take logarithmic time.
-
-This example is based on a similar example found in the ["Sofware Foundations"](https://softwarefoundations.cis.upenn.edu/vfa-current/SearchTree.html)
-book (volume 3).
--/
-
-/-!
-We use `Nat` as the key type in our implementation of BSTs,
-since it has a convenient total order with lots of theorems and automation available.
-We leave as an exercise to the reader the generalization to arbitrary types.
--/
-
-inductive Tree (β : Type v) where
-  | leaf
-  | node (left : Tree β) (key : Nat) (value : β) (right : Tree β)
-  deriving Repr
-
-/-!
-The function `contains` returns `true` iff the given tree contains the key `k`.
--/
-def Tree.contains (t : Tree β) (k : Nat) : Bool :=
-  match t with
-  | leaf => false
-  | node left key value right =>
-    if k < key then
-      left.contains k
-    else if key < k then
-      right.contains k
-    else
-      true
-
-/-!
-`t.find? k` returns `some v` if `v` is the value bound to key `k` in the tree `t`. It returns `none` otherwise.
--/
-def Tree.find? (t : Tree β) (k : Nat) : Option β :=
-  match t with
-  | leaf => none
-  | node left key value right =>
-    if k < key then
-      left.find? k
-    else if key < k then
-      right.find? k
-    else
-      some value
-
-/-!
-`t.insert k v` is the map containing all the bindings of `t` along with a binding of `k` to `v`.
--/
-def Tree.insert (t : Tree β) (k : Nat) (v : β) : Tree β :=
-  match t with
-  | leaf => node leaf k v leaf
-  | node left key value right =>
-    if k < key then
-      node (left.insert k v) key value right
-    else if key < k then
-      node left key value (right.insert k v)
-    else
-      node left k v right
-/-!
-Let's add a new operation to our tree: converting it to an association list that contains the key--value bindings from the tree stored as pairs.
-If that list is sorted by the keys, then any two trees that represent the same map would be converted to the same list.
-Here's a function that does so with an in-order traversal of the tree.
--/
-def Tree.toList (t : Tree β) : List (Nat × β) :=
-  match t with
-  | leaf => []
-  | node l k v r => l.toList ++ [(k, v)] ++ r.toList
-
-#eval Tree.leaf.insert 2 "two"
-      |>.insert 3 "three"
-      |>.insert 1 "one"
-
-#eval Tree.leaf.insert 2 "two"
-      |>.insert 3 "three"
-      |>.insert 1 "one"
-      |>.toList
-
-/-!
-The implemention of `Tree.toList` is inefficient because of how it uses the `++` operator.
-On a balanced tree its running time is linearithmic, because it does a linear number of
-concatentations at each level of the tree. On an unbalanced tree it's quadratic time.
-Here's a tail-recursive implementation than runs in linear time, regardless of whether the tree is balanced:
--/
-def Tree.toListTR (t : Tree β) : List (Nat × β) :=
-  go t []
-where
-  go (t : Tree β) (acc : List (Nat × β)) : List (Nat × β) :=
-    match t with
-    | leaf => acc
-    | node l k v r => go l ((k, v) :: go r acc)
-
-/-!
-We now prove that `t.toList` and `t.toListTR` return the same list.
-The proof is on induction, and as we used the auxiliary function `go`
-to define `Tree.toListTR`, we use the auxiliary theorem `go` to prove the theorem.
-
-The proof of the auxiliary theorem is by induction on `t`.
-The `generalizing acc` modifier instructs Lean to revert `acc`, apply the
-induction theorem for `Tree`s, and then reintroduce `acc` in each case.
-By using `generalizing`, we obtain the more general induction hypotheses
-
-- `left_ih : ∀ acc, toListTR.go left acc = toList left ++ acc`
-
-- `right_ih : ∀ acc, toListTR.go right acc = toList right ++ acc`
-
-Recall that the combinator `tac <;> tac'` runs `tac` on the main goal and `tac'` on each produced goal,
-concatenating all goals produced by `tac'`. In this theorem, we use it to apply
-`simp` and close each subgoal produced by the `induction` tactic.
-
-The `simp` parameters `toListTR.go` and `toList` instruct the simplifier to try to reduce
-and/or apply auto generated equation theorems for these two functions.
-The parameter `*` intructs the simplifier to use any equation in a goal as rewriting rules.
-In this particular case, `simp` uses the induction hypotheses as rewriting rules.
-Finally, the parameter `List.append_assoc` intructs the simplifier to use the
-`List.append_assoc` theorem as a rewriting rule.
--/
-theorem Tree.toList_eq_toListTR (t : Tree β)
-        : t.toList = t.toListTR := by
-  simp [toListTR, go t []]
-where
-  go (t : Tree β) (acc : List (Nat × β))
-     : toListTR.go t acc = t.toList ++ acc := by
-    induction t generalizing acc <;>
-      simp [toListTR.go, toList, *, List.append_assoc]
-
-/-!
-The `[csimp]` annotation instructs the Lean code generator to replace
-any `Tree.toList` with `Tree.toListTR` when generating code.
--/
-@[csimp] theorem Tree.toList_eq_toListTR_csimp
-                 : @Tree.toList = @Tree.toListTR := by
-  funext β t
-  apply toList_eq_toListTR
-
-/-!
-The implementations of `Tree.find?` and `Tree.insert` assume that values of type tree obey the BST invariant:
-for any non-empty node with key `k`, all the values of the `left` subtree are less than `k` and all the values
-of the right subtree are greater than `k`. But that invariant is not part of the definition of tree.
-
-So, let's formalize the BST invariant. Here's one way to do so. First, we define a helper `ForallTree`
-to express that idea that a predicate holds at every node of a tree:
--/
-inductive ForallTree (p : Nat → β → Prop) : Tree β → Prop
-  | leaf : ForallTree p .leaf
-  | node :
-     ForallTree p left →
-     p key value →
-     ForallTree p right →
-     ForallTree p (.node left key value right)
-
-/-!
-Second, we define the BST invariant:
-An empty tree is a BST.
-A non-empty tree is a BST if all its left nodes have a lesser key, its right nodes have a greater key, and the left and right subtrees are themselves BSTs.
--/
-inductive BST : Tree β → Prop
-  | leaf : BST .leaf
-  | node :
-     ForallTree (fun k v => k < key) left →
-     ForallTree (fun k v => key < k) right →
-     BST left → BST right →
-     BST (.node left key value right)
-
-/-!
-We can use the `macro` command to create helper tactics for organizing our proofs.
-The macro `have_eq x y` tries to prove `x = y` using linear arithmetic, and then
-immediately uses the new equality to substitute `x` with `y` everywhere in the goal.
-
-The modifier `local` specifies the scope of the macro.
--/
-/-- The `have_eq lhs rhs` tactic (tries to) prove that `lhs = rhs`,
-    and then replaces `lhs` with `rhs`. -/
-local macro "have_eq " lhs:term:max rhs:term:max : tactic =>
-  `(tactic|
-    (have h : $lhs = $rhs :=
-       -- TODO: replace with linarith
-       by simp_arith at *; apply Nat.le_antisymm <;> assumption
-     try subst $lhs))
-
-/-!
-The `by_cases' e` is just the regular `by_cases` followed by `simp` using all
-hypotheses in the current goal as rewriting rules.
-Recall that the `by_cases` tactic creates two goals. One where we have `h : e` and
-another one containing `h : ¬ e`. The simplier uses the `h` to rewrite `e` to `True`
-in the first subgoal, and `e` to `False` in the second. This is particularly
-useful if `e` is the condition of an `if`-statement.
--/
-/-- `by_cases' e` is a shorthand form `by_cases e <;> simp[*]` -/
-local macro "by_cases' " e:term :  tactic =>
-  `(tactic| by_cases $e <;> simp [*])
-
-
-/-!
-We can use the attribute `[simp]` to instruct the simplifier to reduce given definitions or
-apply rewrite theorems. The `local` modifier limits the scope of this modification to this file.
--/
-attribute [local simp] Tree.insert
-
-/-!
-We now prove that `Tree.insert` preserves the BST invariant using induction and case analysis.
-Recall that the tactic `. tac` focuses on the main goal and tries to solve it using `tac`, or else fails.
-It is used to structure proofs in Lean.
-The notation `‹e›` is just syntax sugar for `(by assumption : e)`. That is, it tries to find a hypothesis `h : e`.
-It is useful to access hypothesis that have auto generated names (aka "inaccessible") names.
--/
-
-theorem Tree.forall_insert_of_forall
-        (h₁ : ForallTree p t) (h₂ : p key value)
-        : ForallTree p (t.insert key value) := by
-  induction h₁ with
-  | leaf => exact .node .leaf h₂ .leaf
-  | node hl hp hr ihl ihr =>
-    rename Nat => k
-    by_cases' key < k
-    . exact .node ihl hp hr
-    . by_cases' k < key
-      . exact .node hl hp ihr
-      . have_eq key k
-        exact .node hl h₂ hr
-
-theorem Tree.bst_insert_of_bst
-        {t : Tree β} (h : BST t) (key : Nat) (value : β)
-        : BST (t.insert key value) := by
-  induction h with
-  | leaf => exact .node .leaf .leaf .leaf .leaf
-  | node h₁ h₂ b₁ b₂ ih₁ ih₂ =>
-    rename Nat => k
-    simp
-    by_cases' key < k
-    . exact .node (forall_insert_of_forall h₁ ‹key < k›) h₂ ih₁ b₂
-    . by_cases' k < key
-      . exact .node h₁ (forall_insert_of_forall h₂ ‹k < key›) b₁ ih₂
-      . have_eq key k
-        exact .node h₁ h₂ b₁ b₂
-
-/-!
-Now, we define the type `BinTree` using a `Subtype` that states that only trees satisfying the BST invariant are `BinTree`s.
--/
-def BinTree (β : Type u) := { t : Tree β // BST t }
-
-def BinTree.mk : BinTree β :=
-  ⟨.leaf, .leaf⟩
-
-def BinTree.contains (b : BinTree β) (k : Nat) : Bool :=
-  b.val.contains k
-
-def BinTree.find? (b : BinTree β) (k : Nat) : Option β :=
-  b.val.find? k
-
-def BinTree.insert (b : BinTree β) (k : Nat) (v : β) : BinTree β :=
-  ⟨b.val.insert k v, b.val.bst_insert_of_bst b.property k v⟩
-
-/-!
-Finally, we prove that `BinTree.find?` and `BinTree.insert` satisfy the map properties.
--/
-
-attribute [local simp]
-  BinTree.mk BinTree.contains BinTree.find?
-  BinTree.insert Tree.find? Tree.contains Tree.insert
-
-theorem BinTree.find_mk (k : Nat)
-        : BinTree.mk.find? k = (none : Option β) := by
-  simp
-
-theorem BinTree.find_insert (b : BinTree β) (k : Nat) (v : β)
-        : (b.insert k v).find? k = some v := by
-  let ⟨t, h⟩ := b; simp
-  induction t with simp
-  | node left key value right ihl ihr =>
-    by_cases' k < key
-    . cases h; apply ihl; assumption
-    . by_cases' key < k
-      cases h; apply ihr; assumption
-
-theorem BinTree.find_insert_of_ne (b : BinTree β) (h : k ≠ k') (v : β)
-        : (b.insert k v).find? k' = b.find? k' := by
-  let ⟨t, h⟩ := b; simp
-  induction t with simp
-  | leaf =>
-    split <;> simp <;> split <;> simp
-    have_eq k k'
-    contradiction
-  | node left key value right ihl ihr =>
-    let .node hl hr bl br := h
-    specialize ihl bl
-    specialize ihr br
-    by_cases' k < key; by_cases' key < k
-    have_eq key k
-    by_cases' k' < k; by_cases' k  < k'
-    have_eq k k'
-    contradiction

doc/examples/bintree.lean.md

@@ -1,5 +0,0 @@
-(this example is rendered by Alectryon in the CI)
-
-```lean
-{{#include bintree.lean}}
-```

doc/examples/deBruijn.lean

@@ -1,163 +0,0 @@
-/-!
-# Dependent de Bruijn Indices
-
-In this example, we represent program syntax terms in a type family parameterized by a list of types,
-representing the typing context, or information on which free variables are in scope and what
-their types are.
-
-
-Remark: this example is based on an example in the book [Certified Programming with Dependent Types](http://adam.chlipala.net/cpdt/) by Adam Chlipala.
--/
-
-/-!
-Programmers who move to statically typed functional languages from scripting languages
-often complain about the requirement that every element of a list have the same type. With
-fancy type systems, we can partially lift this requirement. We can index a list type with a
-“type-level” list that explains what type each element of the list should have. This has been
-done in a variety of ways in Haskell using type classes, and we can do it much more cleanly
-and directly in Lean.
-
-We parameterize our heterogeneous lists by at type `α` and an `α`-indexed type `β`.
--/
-
-inductive HList {α : Type v} (β : α → Type u) : List α → Type (max u v)
-  | nil  : HList β []
-  | cons : β i → HList β is → HList β (i::is)
-
-/-!
-We overload the `List.cons` notation `::` so we can also use it to create
-heterogeneous lists.
--/
-infix:67 " :: " => HList.cons
-
-/-! We similarly overload the `List` notation `[]` for the empty heterogeneous list. -/
-notation "[" "]" => HList.nil
-
-/-!
-Variables are represented in a way isomorphic to the natural numbers, where
-number 0 represents the first element in the context, number 1 the second element, and so
-on. Actually, instead of numbers, we use the `Member` inductive family.
-
-The value of type `Member a as` can be viewed as a certificate that `a` is
-an element of the list `as`. The constructor `Member.head` says that `a`
-is in the list if the list begins with it. The constructor `Member.tail`
-says that if `a` is in the list `bs`, it is also in the list `b::bs`.
--/
-inductive Member : α → List α → Type
-  | head : Member a (a::as)
-  | tail : Member a bs → Member a (b::bs)
-
-/-!
-Given a heterogeneous list `HList β is` and value of type `Member i is`, `HList.get`
-retrieves an element of type `β i` from the list.
-The pattern `.head` and `.tail h` are sugar for `Member.head` and `Member.tail h` respectively.
-Lean can infer the namespace using the expected type.
--/
-def HList.get : HList β is → Member i is → β i
-  | a::as, .head => a
-  | a::as, .tail h => as.get h
-
-/-!
-Here is the definition of the simple type system for our programming language, a simply typed
-lambda calculus with natural numbers as the base type.
--/
-inductive Ty where
-  | nat
-  | fn : Ty → Ty → Ty
-
-/-!
-We can write a function to translate `Ty` values to a Lean type
-— remember that types are first class, so can be calculated just like any other value.
-We mark `Ty.denote` as `[reducible]` to make sure the typeclass resolution procedure can
-unfold/reduce it. For example, suppose Lean is trying to synthesize a value for the instance
-`Add (Ty.denote Ty.nat)`. Since `Ty.denote` is marked as `[reducible]`,
-the typeclass resolution procedure can reduce `Ty.denote Ty.nat` to `Nat`, and use
-the builtin instance for `Add Nat` as the solution.
-
-Recall that the term `a.denote` is sugar for `denote a` where `denote` is the function being defined.
-We call it the "dot notation".
--/
-@[reducible] def Ty.denote : Ty → Type
-  | nat    => Nat
-  | fn a b => a.denote → b.denote
-
-/-!
-Here is the definition of the `Term` type, including variables, constants, addition,
-function application and abstraction, and let binding of local variables.
-Since `let` is a keyword in Lean, we use the "escaped identifier" `«let»`.
-You can input the unicode (French double quotes) using `\f<<` (for `«`) and `\f>>` (for `»`).
-The term `Term ctx .nat` is sugar for `Term ctx Ty.nat`, Lean infers the namespace using the expected type.
--/
-inductive Term : List Ty → Ty → Type
-  | var   : Member ty ctx → Term ctx ty
-  | const : Nat → Term ctx .nat
-  | plus  : Term ctx .nat → Term ctx .nat → Term ctx .nat
-  | app   : Term ctx (.fn dom ran) → Term ctx dom → Term ctx ran
-  | lam   : Term (dom :: ctx) ran → Term ctx (.fn dom ran)
-  | «let» : Term ctx ty₁ → Term (ty₁ :: ctx) ty₂ → Term ctx ty₂
-
-/-!
-Here are two example terms encoding, the first addition packaged as a two-argument
-curried function, and the second of a sample application of addition to constants.
-
-The command `open Ty Term Member` opens the namespaces `Ty`, `Term`, and `Member`. Thus,
-you can write `lam` instead of `Term.lam`.
--/
-open Ty Term Member
-def add : Term [] (fn nat (fn nat nat)) :=
-  lam (lam (plus (var (tail head)) (var head)))
-
-def three_the_hard_way : Term [] nat :=
-  app (app add (const 1)) (const 2)
-
-/-!
-Since dependent typing ensures that any term is well-formed in its context and has a particular type,
-it is easy to translate syntactic terms into Lean values.
-
-The attribute `[simp]` instructs Lean to always try to unfold `Term.denote` applications when one applies
-the `simp` tactic. We also say this is a hint for the Lean term simplifier.
--/
-@[simp] def Term.denote : Term ctx ty → HList Ty.denote ctx → ty.denote
-  | var h,     env => env.get h
-  | const n,   _   => n
-  | plus a b,  env => a.denote env + b.denote env
-  | app f a,   env => f.denote env (a.denote env)
-  | lam b,     env => fun x => b.denote (x :: env)
-  | «let» a b, env => b.denote (a.denote env :: env)
-
-/-!
-You can show that the denotation of `three_the_hard_way` is indeed `3` using reflexivity.
--/
-example : three_the_hard_way.denote [] = 3 :=
-  rfl
-
-/-!
-We now define the constant folding optimization that traverses a term if replaces subterms such as
-`plus (const m) (const n)` with `const (n+m)`.
--/
-@[simp] def Term.constFold : Term ctx ty → Term ctx ty
-  | const n   => const n
-  | var h     => var h
-  | app f a   => app f.constFold a.constFold
-  | lam b     => lam b.constFold
-  | «let» a b => «let» a.constFold b.constFold
-  | plus a b  =>
-    match a.constFold, b.constFold with
-    | const n, const m => const (n+m)
-    | a',      b'      => plus a' b'
-
-/-!
-The correctness of the `Term.constFold` is proved using induction, case-analysis, and the term simplifier.
-We prove all cases but the one for `plus` using `simp [*]`. This tactic instructs the term simplifier to
-use hypotheses such as `a = b` as rewriting/simplications rules.
-We use the `split` to break the nested `match` expression in the `plus` case into two cases.
-The local variables `iha` and `ihb` are the induction hypotheses for `a` and `b`.
-The modifier `←` in a term simplifier argument instructs the term simplier to use the equation as a rewriting rule in
-the "reverse direction". That is, given `h : a = b`, `← h` instructs the term simplifier to rewrite `b` subterms to `a`.
--/
-theorem Term.constFold_sound (e : Term ctx ty) : e.constFold.denote env = e.denote env := by
-  induction e with simp [*]
-  | plus a b iha ihb =>
-    split
-    next he₁ he₂ => simp [← iha, ← ihb, he₁, he₂]
-    next => simp [iha, ihb]

doc/examples/deBruijn.lean.md

@@ -1,5 +0,0 @@
-(this example is rendered by Alectryon in the CI)
-
-```lean
-{{#include deBruijn.lean}}
-```

doc/examples/interp.lean

@@ -1,152 +0,0 @@
-/-!
-# The Well-Typed Interpreter
-
-In this example, we build an interpreter for a simple functional programming language,
-with variables, function application, binary operators and an `if...then...else` construct.
-We will use the dependent type system to ensure that any programs which can be represented are well-typed.
-
-Remark: this example is based on an example found in the Idris manual.
--/
-
-/-!
-Vectors
---------
-
-A `Vector` is a list of size `n` whose elements belong to a type `α`.
--/
-
-inductive Vector (α : Type u) : Nat → Type u
-  | nil : Vector α 0
-  | cons : α → Vector α n → Vector α (n+1)
-
-/-!
-We can overload the `List.cons` notation `::` and use it to create `Vector`s.
--/
-infix:67 " :: " => Vector.cons
-
-/-!
-Now, we define the types of our simple functional language.
-We have integers, booleans, and functions, represented by `Ty`.
--/
-inductive Ty where
-  | int
-  | bool
-  | fn (a r : Ty)
-
-/-!
-We can write a function to translate `Ty` values to a Lean type
-— remember that types are first class, so can be calculated just like any other value.
-We mark `Ty.interp` as `[reducible]` to make sure the typeclass resolution procedure can
-unfold/reduce it. For example, suppose Lean is trying to synthesize a value for the instance
-`Add (Ty.interp Ty.int)`. Since `Ty.interp` is marked as `[reducible]`,
-the typeclass resolution procedure can reduce `Ty.interp Ty.int` to `Int`, and use
-the builtin instance for `Add Int` as the solution.
--/
-@[reducible] def Ty.interp : Ty → Type
-  | int    => Int
-  | bool   => Bool
-  | fn a r => a.interp → r.interp
-
-/-!
-Expressions are indexed by the types of the local variables, and the type of the expression itself.
--/
-inductive HasType : Fin n → Vector Ty n → Ty → Type where
-  | stop : HasType 0 (ty :: ctx) ty
-  | pop  : HasType k ctx ty → HasType k.succ (u :: ctx) ty
-
-inductive Expr : Vector Ty n → Ty → Type where
-  | var   : HasType i ctx ty → Expr ctx ty
-  | val   : Int → Expr ctx Ty.int
-  | lam   : Expr (a :: ctx) ty → Expr ctx (Ty.fn a ty)
-  | app   : Expr ctx (Ty.fn a ty) → Expr ctx a → Expr ctx ty
-  | op    : (a.interp → b.interp → c.interp) → Expr ctx a → Expr ctx b → Expr ctx c
-  | ife   : Expr ctx Ty.bool → Expr ctx a → Expr ctx a → Expr ctx a
-  | delay : (Unit → Expr ctx a) → Expr ctx a
-
-/-!
-We use the command `open` to create the aliases `stop` and `pop` for `HasType.stop` and `HasType.pop` respectively.
--/
-open HasType (stop pop)
-
-/-!
-Since expressions are indexed by their type, we can read the typing rules of the language from the definitions of the constructors.
-Let us look at each constructor in turn.
-
-We use a nameless representation for variables — they are de Bruijn indexed.
-Variables are represented by a proof of their membership in the context, `HasType i ctx ty`,
-which is a proof that variable `i` in context `ctx` has type `ty`.
-
-We can treat `stop` as a proof that the most recently defined variable is well-typed,
-and `pop n` as a proof that, if the `n`th most recently defined variable is well-typed, so is the `n+1`th.
-In practice, this means we use `stop` to refer to the most recently defined variable,
-`pop stop` to refer to the next, and so on, via the `Expr.var` constructor.
-
-A value `Expr.val` carries a concrete representation of an integer.
-
-A lambda `Expr.lam` creates a function. In the scope of a function ot type `Ty.fn a ty`, there is a
-new local variable of type `a`.
-
-A function application `Expr.app` produces a value of type `ty` given a function from `a` to `ty` and a value of type `a`.
-
-The constructor `Expr.op` allows us to use arbitrary binary operators, where the type of the operator informs what the types of the arguments must be.
-
-Finally, the constructor `Exp.ife` represents a `if-then-else` expression. The condition is a Boolean, and each branch must have the same type.
-
-The auxiliary constructor `Expr.delay` is used to delay evaluation.
--/
-
-
-/-!
-When we evaluate an `Expr`, we’ll need to know the values in scope, as well as their types. `Env` is an environment,
-indexed over the types in scope. Since an environment is just another form of list, albeit with a strongly specified connection
-to the vector of local variable types, we overload again the notation `::` so that we can use the usual list syntax.
-Given a proof that a variable is defined in the context, we can then produce a value from the environment.
--/
-inductive Env : Vector Ty n → Type where
-  | nil  : Env Vector.nil
-  | cons : Ty.interp a → Env ctx → Env (a :: ctx)
-
-infix:67 " :: " => Env.cons
-
-def Env.lookup : HasType i ctx ty → Env ctx → ty.interp
-  | stop,  x :: xs => x
-  | pop k, x :: xs => lookup k xs
-
-/-!
-Given this, an interpreter is a function which translates an `Expr` into a Lean value with respect to a specific environment.
--/
-def Expr.interp (env : Env ctx) : Expr ctx ty → ty.interp
-  | var i     => env.lookup i
-  | val x     => x
-  | lam b     => fun x => b.interp (Env.cons x env)
-  | app f a   => f.interp env (a.interp env)
-  | op o x y  => o (x.interp env) (y.interp env)
-  | ife c t e => if c.interp env then t.interp env else e.interp env
-  | delay a   => (a ()).interp env
-
-open Expr
-
-/-!
-We can make some simple test functions. Firstly, adding two inputs `fun x y => y + x` is written as follows.
--/
-
-def add : Expr ctx (Ty.fn Ty.int (Ty.fn Ty.int Ty.int)) :=
-  lam (lam (op (·+·) (var stop) (var (pop stop))))
-
-#eval add.interp Env.nil 10 20
-
-/-!
-More interestingly, a factorial function fact (e.g. `fun x => if (x == 0) then 1 else (fact (x-1) * x)`), can be written as.
-Note that this is a recursive (non-terminating) definition. For every input value, the interpreter terminates, but the
-definition itself is non-terminating. We use two tricks to make sure Lean accepts it. First, we use the auxiliary constructor
-`Expr.delay` to delay its unfolding. Second, we add the annotation `decreasing_by sorry` which can be viwed as
-"trust me, this recursive definition makes sense". Recall that `sorry` is an unsound axiom in Lean.
--/
-
-def fact : Expr ctx (Ty.fn Ty.int Ty.int) :=
-  lam (ife (op (·==·) (var stop) (val 0))
-           (val 1)
-           (op (·*·) (delay fun _ => app fact (op (·-·) (var stop) (val 1))) (var stop)))
-  decreasing_by sorry
-
-#eval fact.interp Env.nil 10

doc/examples/interp.lean.md

@@ -1,5 +0,0 @@
-(this example is rendered by Alectryon in the CI)
-
-```lean
-{{#include interp.lean}}
-```

doc/examples/palindromes.lean

@@ -1,122 +0,0 @@
-/-!
-# Palindromes
-
-Palindromes are lists that read the same from left to right and from right to left.
-For example, `[a, b, b, a]` and `[a, h, a]` are palindromes.
-
-We use an inductive predicate to specify whether a list is a palindrome or not.
-Recall that inductive predicates, or inductively defined propositions, are a convenient
-way to specify functions of type `... → Prop`.
-
-This example is a based on an example from the book "The Hitchhiker's Guide to Logical Verification".
--/
-
-inductive Palindrome : List α → Prop where
-  | nil      : Palindrome []
-  | single   : (a : α) → Palindrome [a]
-  | sandwich : (a : α) → Palindrome as → Palindrome ([a] ++ as ++ [a])
-
-/-!
-The definition distinguishes three cases: (1) `[]` is a palindrome; (2) for any element
-`a`, the singleton list `[a]` is a palindrome; (3) for any element `a` and any palindrome
-`[b₁, . . ., bₙ]`, the list `[a, b₁, . . ., bₙ, a]` is a palindrome.
--/
-
-/-!
-We now prove that the reverse of a palindrome is a palindrome using induction on the inductive predicate `h : Palindrome as`.
--/
-theorem palindrome_reverse (h : Palindrome as) : Palindrome as.reverse := by
-  induction h with
-  | nil => exact Palindrome.nil
-  | single a => exact Palindrome.single a
-  | sandwich a h ih => simp; exact Palindrome.sandwich _ ih
-
-/-! If a list `as` is a palindrome, then the reverse of `as` is equal to itself. -/
-theorem reverse_eq_of_palindrome (h : Palindrome as) : as.reverse = as := by
-  induction h with
-  | nil => rfl
-  | single a => rfl
-  | sandwich a h ih => simp [ih]
-
-/-! Note that you can also easily prove `palindrome_reverse` using `reverse_eq_of_palindrome`. -/
-example (h : Palindrome as) : Palindrome as.reverse := by
-  simp [reverse_eq_of_palindrome h, h]
-
-/-!
-Given a nonempty list, the function `List.last` returns its element.
-Note that we use `(by simp)` to prove that `a₂ :: as ≠ []` in the recursive application.
--/
-def List.last : (as : List α) → as ≠ [] → α
-  | [a],         _ => a
-  | _::a₂:: as, _ => (a₂::as).last (by simp)
-
-/-!
-We use the function `List.last` to prove the following theorem that says that if a list `as` is not empty,
-then removing the last element from `as` and appending it back is equal to `as`.
-We use the attribute `@[simp]` to instruct the `simp` tactic to use this theorem as a simplification rule.
--/
-@[simp] theorem List.dropLast_append_last (h : as ≠ []) : as.dropLast ++ [as.last h] = as := by
-  match as with
-  | [] => contradiction
-  | [a] => simp_all [last, dropLast]
-  | a₁ :: a₂ :: as =>
-    simp [last, dropLast]
-    exact dropLast_append_last (as := a₂ :: as) (by simp)
-
-/-!
-We now define the following auxiliary induction principle for lists using well-founded recursion on `as.length`.
-We can read it as follows, to prove `motive as`, it suffices to show that: (1) `motive []`; (2) `motive [a]` for any `a`;
-(3) if `motive as` holds, then `motive ([a] ++ as ++ [b])` also holds for any `a`, `b`, and `as`.
-Note that the structure of this induction principle is very similar to the `Palindrome` inductive predicate.
--/
-theorem List.palindrome_ind (motive : List α → Prop)
-    (h₁ : motive [])
-    (h₂ : (a : α) → motive [a])
-    (h₃ : (a b : α) → (as : List α) → motive as → motive ([a] ++ as ++ [b]))
-    (as : List α)
-    : motive as :=
-  match as with
-  | []  => h₁
-  | [a] => h₂ a
-  | a₁::a₂::as' =>
-    have ih := palindrome_ind motive h₁ h₂ h₃ (a₂::as').dropLast
-    have : [a₁] ++ (a₂::as').dropLast ++ [(a₂::as').last (by simp)] = a₁::a₂::as' := by simp
-    this ▸ h₃ _ _ _ ih
-termination_by _ as => as.length
-
-/-!
-We use our new induction principle to prove that if `as.reverse = as`, then `Palindrome as` holds.
-Note that we use the `using` modifier to instruct the `induction` tactic to use this induction principle
-instead of the default one for lists.
--/
-theorem List.palindrome_of_eq_reverse (h : as.reverse = as) : Palindrome as := by
-  induction as using palindrome_ind
-  next   => exact Palindrome.nil
-  next a => exact Palindrome.single a
-  next a b as ih =>
-    have : a = b := by simp_all
-    subst this
-    have : as.reverse = as := by simp_all
-    exact Palindrome.sandwich a (ih this)
-
-/-!
-We now define a function that returns `true` iff `as` is a palindrome.
-The function assumes that the type `α` has decidable equality. We need this assumption
-because we need to compare the list elements.
--/
-def List.isPalindrome [DecidableEq α] (as : List α) : Bool :=
-    as.reverse = as
-
-/-!
-It is straightforward to prove that `isPalindrome` is correct using the previously proved theorems.
--/
-theorem List.isPalindrome_correct [DecidableEq α] (as : List α) : as.isPalindrome ↔ Palindrome as := by
-  simp [isPalindrome]
-  exact Iff.intro (fun h => palindrome_of_eq_reverse h) (fun h => reverse_eq_of_palindrome h)
-
-#eval [1, 2, 1].isPalindrome
-#eval [1, 2, 3, 1].isPalindrome
-
-example : [1, 2, 1].isPalindrome := rfl
-example : [1, 2, 2, 1].isPalindrome := rfl
-example : ![1, 2, 3, 1].isPalindrome := rfl

doc/examples/palindromes.lean.md

@@ -1,5 +0,0 @@
-(this example is rendered by Alectryon in the CI)
-
-```lean
-{{#include palindromes.lean}}
-```

doc/examples/phoas.lean

@@ -1,239 +0,0 @@
-/-!
-# Parametric Higher-Order Abstract Syntax
-
-In contrast to first-order encodings, higher-order encodings avoid explicit modeling of variable identity.
-Instead, the binding constructs of an object language (the language being
-formalized) can be represented using the binding constructs of the meta language (the language in which the formalization is done).
-The best known higher-order encoding is called higher-order abstract syntax (HOAS),
-and we can start by attempting to apply it directly in Lean.
-
-Remark: this example is based on an example in the book [Certified Programming with Dependent Types](http://adam.chlipala.net/cpdt/) by Adam Chlipala.
--/
-
-/-!
-Here is the definition of the simple type system for our programming language, a simply typed
-lambda calculus with natural numbers as the base type.
--/
-inductive Ty where
-  | nat
-  | fn : Ty → Ty → Ty
-
-/-!
-We can write a function to translate `Ty` values to a Lean type
-— remember that types are first class, so can be calculated just like any other value.
-We mark `Ty.denote` as `[reducible]` to make sure the typeclass resolution procedure can
-unfold/reduce it. For example, suppose Lean is trying to synthesize a value for the instance
-`Add (Ty.denote Ty.nat)`. Since `Ty.denote` is marked as `[reducible]`,
-the typeclass resolution procedure can reduce `Ty.denote Ty.nat` to `Nat`, and use
-the builtin instance for `Add Nat` as the solution.
-
-Recall that the term `a.denote` is sugar for `denote a` where `denote` is the function being defined.
-We call it the "dot notation".
--/
-@[reducible] def Ty.denote : Ty → Type
-  | nat    => Nat
-  | fn a b => a.denote → b.denote
-
-/-!
-With HOAS, each object language binding construct is represented with a function of
-the meta language. Here is what we get if we apply that idea within an inductive definition
-of term syntax. However a naive encondig in Lean fails to meet the strict positivity restrictions
-imposed by the Lean kernel. An alternate higher-order encoding is parametric HOAS, as introduced by Washburn
-and Weirich for Haskell and tweaked by Adam Chlipala for use in Coq. The key idea is to parameterize the
-declaration by a type family `rep` standing for a "representation of variables."
--/
-inductive Term' (rep : Ty → Type) : Ty → Type
-  | var   : rep ty → Term' rep ty
-  | const : Nat → Term' rep .nat
-  | plus  : Term' rep .nat → Term' rep .nat → Term' rep .nat
-  | lam   : (rep dom → Term' rep ran) → Term' rep (.fn dom ran)
-  | app   : Term' rep (.fn dom ran) → Term' rep dom → Term' rep ran
-  | let   : Term' rep ty₁ → (rep ty₁ → Term' rep ty₂) → Term' rep ty₂
-
-/-!
-Lean accepts this definition because our embedded functions now merely take variables as
-arguments, instead of arbitrary terms. One might wonder whether there is an easy loophole
-to exploit here, instantiating the parameter `rep` as term itself. However, to do that, we
-would need to choose a variable representation for this nested mention of term, and so on
-through an infinite descent into term arguments.
-
-We write the final type of a closed term using polymorphic quantification over all possible
-choices of `rep` type family
--/
-
-open Ty (nat fn)
-
-namespace FirstTry
-
-def Term (ty : Ty) := (rep : Ty → Type) → Term' rep ty
-
-/-!
-In the next two example, note how each is written as a function over a `rep` choice,
-such that the specific choice has no impact on the structure of the term.
--/
-def add : Term (fn nat (fn nat nat)) := fun _rep =>
-  .lam fun x => .lam fun y => .plus (.var x) (.var y)
-
-def three_the_hard_way : Term nat := fun rep =>
-  .app (.app (add rep) (.const 1)) (.const 2)
-
-end FirstTry
-
-/-!
-The argument `rep` does not even appear in the function body for `add`. How can that be?
-By giving our terms expressive types, we allow Lean to infer many arguments for us. In fact,
-we do not even need to name the `rep` argument! By using Lean implicit arguments and lambdas,
-we can completely hide `rep` in these examples.
--/
-
-def Term (ty : Ty) := {rep : Ty → Type} → Term' rep ty
-
-def add : Term (fn nat (fn nat nat)) :=
-  .lam fun x => .lam fun y => .plus (.var x) (.var y)
-
-def three_the_hard_way : Term nat :=
-  .app (.app add (.const 1)) (.const 2)
-
-/-!
-It may not be at all obvious that the PHOAS representation admits the crucial computable
-operations. The key to effective deconstruction of PHOAS terms is one principle: treat
-the `rep` parameter as an unconstrained choice of which data should be annotated on each
-variable. We will begin with a simple example, that of counting how many variable nodes
-appear in a PHOAS term. This operation requires no data annotated on variables, so we
-simply annotate variables with `Unit` values. Note that, when we go under binders in the
-cases for `lam` and `let`, we must provide the data value to annotate on the new variable we
-pass beneath. For our current choice of `Unit` data, we always pass `()`.
--/
-
-def countVars : Term' (fun _ => Unit) ty → Nat
-  | .var _    => 1
-  | .const _  => 0
-  | .plus a b => countVars a + countVars b
-  | .app f a  => countVars f + countVars a
-  | .lam b    => countVars (b ())
-  | .let a b  => countVars a + countVars (b ())
-
-/-! We can now easily prove that `add` has two variables by using reflexivity -/
-
-example : countVars add = 2 :=
-  rfl
-
-/-!
-Here is another example, translating PHOAS terms into strings giving a first-order rendering.
-To implement this translation, the key insight is to tag variables with strings, giving their names.
-The function takes as an additional input `i` which is used to create variable names for binders.
-We also use the string interpolation available in Lean. For example, `s!"x_{i}"` is expanded to
-`"x_" ++ toString i`.
--/
-def pretty (e : Term' (fun _ => String) ty) (i : Nat := 1) : String :=
-  match e with
-  | .var s     => s
-  | .const n   => toString n
-  | .app f a   => s!"({pretty f i} {pretty a i})"
-  | .plus a b  => s!"({pretty a i} + {pretty b i})"
-  | .lam f     =>
-    let x := s!"x_{i}"
-    s!"(fun {x} => {pretty (f x) (i+1)})"
-  | .let a b  =>
-    let x := s!"x_{i}"
-    s!"(let {x} := {pretty a i}; => {pretty (b x) (i+1)}"
-
-#eval pretty three_the_hard_way
-
-/-!
-It is not necessary to convert to a different representation to support many common
-operations on terms. For instance, we can implement substitution of terms for variables.
-The key insight here is to tag variables with terms, so that, on encountering a variable, we
-can simply replace it by the term in its tag. We will call this function initially on a term
-with exactly one free variable, tagged with the appropriate substitute. During recursion,
-new variables are added, but they are only tagged with their own term equivalents. Note
-that this function squash is parameterized over a specific `rep` choice.
--/
-def squash : Term' (Term' rep) ty → Term' rep ty
- | .var e    => e
- | .const n  => .const n
- | .plus a b => .plus (squash a) (squash b)
- | .lam f    => .lam fun x => squash (f (.var x))
- | .app f a  => .app (squash f) (squash a)
- | .let a b  => .let (squash a) fun x => squash (b (.var x))
-
-/-!
-To define the final substitution function over terms with single free variables, we define
-`Term1`, an analogue to Term that we defined before for closed terms.
--/
-def Term1 (ty1 ty2 : Ty) := {rep : Ty → Type} → rep ty1 → Term' rep ty2
-
-/-!
-Substitution is defined by (1) instantiating a `Term1` to tag variables with terms and (2)
-applying the result to a specific term to be substituted. Note how the parameter `rep` of
-`squash` is instantiated: the body of `subst` is itself a polymorphic quantification over `rep`,
-standing for a variable tag choice in the output term; and we use that input to compute a
-tag choice for the input term.
--/
-
-def subst (e : Term1 ty1 ty2) (e' : Term ty1) : Term ty2 :=
-  squash (e e')
-
-/-!
-We can view `Term1` as a term with hole. In the following example,
-`(fun x => plus (var x) (const 5))` can be viewed as the term `plus _ (const 5)` where
-the hole `_` is instantiated by `subst` with `three_the_hard_way`
--/
-
-#eval pretty <| subst (fun x => .plus (.var x) (.const 5)) three_the_hard_way
-
-/-!
-One further development, which may seem surprising at first,
-is that we can also implement a usual term denotation function,
-when we tag variables with their denotations.
-
-The attribute `[simp]` instructs Lean to always try to unfold `denote` applications when one applies
-the `simp` tactic. We also say this is a hint for the Lean term simplifier.
--/
-@[simp] def denote : Term' Ty.denote ty → ty.denote
-  | .var x    => x
-  | .const n  => n
-  | .plus a b => denote a + denote b
-  | .app f a  => denote f (denote a)
-  | .lam f    => fun x => denote (f x)
-  | .let a b  => denote (b (denote a))
-
-example : denote three_the_hard_way = 3 :=
-  rfl
-
-/-!
-To summarize, the PHOAS representation has all the expressive power of more
-standard encodings (e.g., using de Bruijn indices), and a variety of translations are actually much more pleasant to
-implement than usual, thanks to the novel ability to tag variables with data.
--/
-
-/-!
-We now define the constant folding optimization that traverses a term if replaces subterms such as
-`plus (const m) (const n)` with `const (n+m)`.
--/
-@[simp] def constFold : Term' rep ty → Term' rep ty
-  | .var x    => .var x
-  | .const n  => .const n
-  | .app f a  => .app (constFold f) (constFold a)
-  | .lam f    => .lam fun x => constFold (f x)
-  | .let a b  => .let (constFold a) fun x => constFold (b x)
-  | .plus a b =>
-    match constFold a, constFold b with
-    | .const n, .const m => .const (n+m)
-    | a',       b'       => .plus a' b'
-
-/-!
-The correctness of the `constFold` is proved using induction, case-analysis, and the term simplifier.
-We prove all cases but the one for `plus` using `simp [*]`. This tactic instructs the term simplifier to
-use hypotheses such as `a = b` as rewriting/simplications rules.
-We use the `split` to break the nested `match` expression in the `plus` case into two cases.
-The local variables `iha` and `ihb` are the induction hypotheses for `a` and `b`.
-The modifier `←` in a term simplifier argument instructs the term simplier to use the equation as a rewriting rule in
-the "reverse direction. That is, given `h : a = b`, `← h` instructs the term simplifier to rewrite `b` subterms to `a`.
--/
-theorem constFold_sound (e : Term' Ty.denote ty) : denote (constFold e) = denote e := by
-  induction e with simp [*]
-  | plus a b iha ihb =>
-    split
-    next he₁ he₂ => simp [← iha, ← ihb, he₁, he₂]
-    next => simp [iha, ihb]

doc/examples/phoas.lean.md

@@ -1,5 +0,0 @@
-(this example is rendered by Alectryon in the CI)
-
-```lean
-{{#include phoas.lean}}
-```

doc/examples/tc.lean

@@ -1,119 +0,0 @@
-/-!
-# A Certified Type Checker
-
-In this example, we build a certified type checker for a simple expression
-language.
-
-Remark: this example is based on an example in the book [Certified Programming with Dependent Types](http://adam.chlipala.net/cpdt/) by Adam Chlipala.
--/
-inductive Expr where
-  | nat  : Nat → Expr
-  | plus : Expr → Expr → Expr
-  | bool : Bool → Expr
-  | and  : Expr → Expr → Expr
-
-/-!
-We define a simple language of types using the inductive datatype `Ty`, and
-its typing rules using the inductive predicate `HasType`.
--/
-inductive Ty where
-  | nat
-  | bool
-  deriving DecidableEq
-
-inductive HasType : Expr → Ty → Prop
-  | nat  : HasType (.nat v) .nat
-  | plus : HasType a .nat → HasType b .nat → HasType (.plus a b) .nat
-  | bool : HasType (.bool v) .bool
-  | and  : HasType a .bool → HasType b .bool → HasType (.and a b) .bool
-
-/-!
-We can easily show that if `e` has type `t₁` and type `t₂`, then `t₁` and `t₂` must be equal
-by using the the `cases` tactic. This tactic creates a new subgoal for every constructor,
-and automatically discharges unreachable cases. The tactic combinator `tac₁ <;> tac₂` applies
-`tac₂` to each subgoal produced by `tac₁`. Then, the tactic `rfl` is used to close all produced
-goals using reflexivity.
--/
-theorem HasType.det (h₁ : HasType e t₁) (h₂ : HasType e t₂) : t₁ = t₂ := by
-  cases h₁ <;> cases h₂ <;> rfl
-
-/-!
-The inductive type `Maybe p` has two contructors: `found a h` and `unknown`.
-The former contains an element `a : α` and a proof that `a` satisfies the predicate `p`.
-The constructor `unknown` is used to encode "failure".
--/
-
-inductive Maybe (p : α → Prop) where
-  | found : (a : α) → p a → Maybe p
-  | unknown
-
-/-!
-We define a notation for `Maybe` that is similar to the builtin notation for the Lean builtin type `Subtype`.
--/
-notation "{{ " x " | " p " }}" => Maybe (fun x => p)
-
-/-!
-The function `Expr.typeCheck e` returns a type `ty` and a proof that `e` has type `ty`,
-or `unknown`.
-Recall that, `def Expr.typeCheck ...` in Lean is notation for `namespace Expr def typeCheck ... end Expr`.
-The term `.found .nat .nat` is sugar for `Maybe.found Ty.nat HasType.nat`. Lean can infer the namespaces using
-the expected types.
--/
-def Expr.typeCheck (e : Expr) : {{ ty | HasType e ty }} :=
-  match e with
-  | nat ..   => .found .nat .nat
-  | bool ..  => .found .bool .bool
-  | plus a b =>
-    match a.typeCheck, b.typeCheck with
-    | .found .nat h₁, .found .nat h₂ => .found .nat (.plus h₁ h₂)
-    | _, _ => .unknown
-  | and a b =>
-    match a.typeCheck, b.typeCheck with
-    | .found .bool h₁, .found .bool h₂ => .found .bool (.and h₁ h₂)
-    | _, _ => .unknown
-
-theorem Expr.typeCheck_correct (h₁ : HasType e ty) (h₂ : e.typeCheck ≠ .unknown)
-        : e.typeCheck = .found ty h := by
-  revert h₂
-  cases typeCheck e with
-  | found ty' h' => intro; have := HasType.det h₁ h'; subst this; rfl
-  | unknown => intros; contradiction
-
-/-!
-Now, we prove that if `Expr.typeCheck e` returns `Maybe.unknown`, then forall `ty`, `HasType e ty` does not hold.
-The notation `e.typeCheck` is sugar for `Expr.typeCheck e`. Lean can infer this because we explicitly said that `e` has type `Expr`.
-The proof is by induction on `e` and case analysis. The tactic `rename_i` is used to to rename "inaccessible" variables.
-We say a variable is inaccessible if it is introduced by a tactic (e.g., `cases`) or has been shadowed by another variable introduced
-by the user. Note that the tactic `simp [typeCheck]` is applied to all goal generated by the `induction` tactic, and closes
-the cases corresponding to the constructors `Expr.nat` and `Expr.bool`.
--/
-theorem Expr.typeCheck_complete {e : Expr} : e.typeCheck = .unknown → ¬ HasType e ty := by
-  induction e with simp [typeCheck]
-  | plus a b iha ihb =>
-    split
-    next => intros; contradiction
-    next ra rb hnp =>
-      -- Recall that `hnp` is a hypothesis generated by the `split` tactic
-      -- that asserts the previous case was not taken
-      intro h ht
-      cases ht with
-      | plus h₁ h₂ => exact hnp h₁ h₂ (typeCheck_correct h₁ (iha · h₁)) (typeCheck_correct h₂ (ihb · h₂))
-  | and a b iha ihb =>
-    split
-    next => intros; contradiction
-    next ra rb hnp =>
-      intro h ht
-      cases ht with
-      | and h₁ h₂ =>  exact hnp h₁ h₂ (typeCheck_correct h₁ (iha · h₁)) (typeCheck_correct h₂ (ihb · h₂))
-
-/-!
-Finally, we show that type checking for `e` can be decided using `Expr.typeCheck`.
--/
-instance (e : Expr) (t : Ty) : Decidable (HasType e t) :=
-  match h' : e.typeCheck with
-  | .found t' ht' =>
-    if heq : t = t' then
-      isTrue (heq ▸ ht')
-    else
-      isFalse fun ht => heq (HasType.det ht ht')
-  | .unknown => isFalse (Expr.typeCheck_complete h')

doc/examples/tc.lean.md

@@ -1,5 +0,0 @@
-(this example is rendered by Alectryon in the CI)
-
-```lean
-{{#include tc.lean}}
-```

doc/examples/test_single.sh

@@ -1,4 +0,0 @@
-#!/usr/bin/env bash
-source ../../tests/common.sh
-
-exec_check lean -j 0 -Dlinter.all=false "$f"

doc/examples/widgets.lean

@@ -1,216 +0,0 @@
-import Lean
-open Lean Widget
-
-/-!
-# The user-widgets system
-
-Proving and programming are inherently interactive tasks. Lots of mathematical objects and data
-structures are visual in nature. *User widgets* let you associate custom interactive UIs with
-sections of a Lean document. User widgets are rendered in the Lean infoview.
-
-![Rubik's cube](../images/widgets_rubiks.png)
-
-## Trying it out
-
-To try it out, simply type in the following code and place your cursor over the `#widget` command.
--/
-
-@[widget]
-def helloWidget : UserWidgetDefinition where
-  name := "Hello"
-  javascript := "
-    import * as React from 'react';
-    export default function(props) {
-      const name = props.name || 'world'
-      return React.createElement('p', {}, name + '!')
-    }"
-
-#widget helloWidget .null
-
-/-!
-If you want to dive into a full sample right away, check out
-[`RubiksCube`](https://github.com/leanprover/lean4-samples/blob/main/RubiksCube/).
-Below, we'll explain the system piece by piece.
-
-⚠️ WARNING: All of the user widget APIs are **unstable** and subject to breaking changes.
-
-## Widget sources and instances
-
-A *widget source* is a valid JavaScript [ESModule](https://developer.mozilla.org/en-US/docs/Web/JavaScript/Guide/Modules)
-which exports a [React component](https://reactjs.org/docs/components-and-props.html). To access
-React, the module must use `import * as React from 'react'`. Our first example of a widget source
-is of course the value of `helloWidget.javascript`.
-
-We can register a widget source with the `@[widget]` attribute, giving it a friendlier name
-in the `name` field. This is bundled together in a `UserWidgetDefinition`.
-
-A *widget instance* is then the identifier of a `UserWidgetDefinition` (so `` `helloWidget ``,
-not `"Hello"`) associated with a range of positions in the Lean source code. Widget instances
-are stored in the *infotree* in the same manner as other information about the source file
-such as the type of every expression. In our example, the `#widget` command stores a widget instance
-with the entire line as its range. We can think of a widget instance as an instruction for the
-infoview: "when the user places their cursor here, please render the following widget".
-
-Every widget instance also contains a `props : Json` value. This value is passed as an argument
-to the React component. In our first invocation of `#widget`, we set it to `.null`. Try out what
-happens when you type in:
--/
-
-#widget helloWidget (Json.mkObj [("name", "<your name here>")])
-
-/-!
-💡 NOTE: The RPC system presented below does not depend on JavaScript. However the primary use case
-is the web-based infoview in VSCode.
-
-## Querying the Lean server
-
-Besides enabling us to create cool client-side visualizations, user widgets come with the ability
-to communicate with the Lean server. Thanks to this, they have the same metaprogramming capabilities
-as custom elaborators or the tactic framework. To see this in action, let's implement a `#check`
-command as a web input form. This example assumes some familiarity with React.
-
-The first thing we'll need is to create an *RPC method*. Meaning "Remote Procedure Call", this
-is basically a Lean function callable from widget code (possibly remotely over the internet).
-Our method will take in the `name : Name` of a constant in the environment and return its type.
-By convention, we represent the input data as a `structure`. Since it will be sent over from JavaScript,
-we need `FromJson` and `ToJson`. We'll see below why the position field is needed.
--/
-
-structure GetTypeParams where
-  /-- Name of a constant to get the type of. -/
-  name : Name
-  /-- Position of our widget instance in the Lean file. -/
-  pos : Lsp.Position
-  deriving FromJson, ToJson
-
-/-!
-After its arguments, we define the `getType` method. Every RPC method executes in the `RequestM`
-monad and must return a `RequestTask α` where `α` is its "actual" return type. The `Task` is so
-that requests can be handled concurrently. A first guess for `α` might be `Expr`. However,
-expressions in general can be large objects which depend on an `Environment` and `LocalContext`.
-Thus we cannot directly serialize an `Expr` and send it to the widget. Instead, there are two
-options:
-- One is to send a *reference* which points to an object residing on the server. From JavaScript's
-  point of view, references are entirely opaque, but they can be sent back to other RPC methods for
-  further processing.
-- Two is to pretty-print the expression and send its textual representation called `CodeWithInfos`.
-  This representation contains extra data which the infoview uses for interactivity. We take this
-  strategy here.
-
-RPC methods execute in the context of a file, but not any particular `Environment` so they don't
-know about the available `def`initions and `theorem`s. Thus, we need to pass in a position at which
-we want to use the local `Environment`. This is why we store it in `GetTypeParams`. The `withWaitFindSnapAtPos`
-method launches a concurrent computation whose job is to find such an `Environment` and a bit
-more information for us, in the form of a `snap : Snapshot`. With this in hand, we can call
-`MetaM` procedures to find out the type of `name` and pretty-print it.
--/
-
-open Server RequestM in
-@[server_rpc_method]
-def getType (params : GetTypeParams) : RequestM (RequestTask CodeWithInfos) :=
-  withWaitFindSnapAtPos params.pos fun snap => do
-    runTermElabM snap do
-      let name ← resolveGlobalConstNoOverloadCore params.name
-      let some c ← Meta.getConst? name
-        | throwThe RequestError ⟨.invalidParams, s!"no constant named '{name}'"⟩
-      Widget.ppExprTagged c.type
-
-/-!
-## Using infoview components
-
-Now that we have all we need on the server side, let's write the widget source. By importing
-`@leanprover/infoview`, widgets can render UI components used to implement the infoview itself.
-For example, the `<InteractiveCode>` component displays expressions with `term : type` tooltips
-as seen in the goal view. We will use it to implement our custom `#check` display.
-
-⚠️ WARNING: Like the other widget APIs, the infoview JS API is **unstable** and subject to breaking changes.
-
-The code below demonstrates useful parts of the API. To make RPC method calls, we use the `RpcContext`.
-The `useAsync` helper packs the results of a call into an `AsyncState` structure which indicates
-whether the call has resolved successfully, has returned an error, or is still in-flight. Based
-on this we either display an `InteractiveCode` with the type, `mapRpcError` the error in order
-to turn it into a readable message, or show a `Loading..` message, respectively.
--/
-
-@[widget]
-def checkWidget : UserWidgetDefinition where
-  name := "#check as a service"
-  javascript := "
-import * as React from 'react';
-const e = React.createElement;
-import { RpcContext, InteractiveCode, useAsync, mapRpcError } from '@leanprover/infoview';
-
-export default function(props) {
-  const rs = React.useContext(RpcContext)
-  const [name, setName] = React.useState('getType')
-
-  const st = useAsync(() =>
-    rs.call('getType', { name, pos: props.pos }), [name, rs, props.pos])
-
-  const type = st.state === 'resolved' ? st.value && e(InteractiveCode, {fmt: st.value})
-    : st.state === 'rejected' ? e('p', null, mapRpcError(st.error).message)
-    : e('p', null, 'Loading..')
-  const onChange = (event) => { setName(event.target.value) }
-  return e('div', null,
-    e('input', { value: name, onChange }), ' : ', type)
-}
-"
-
-/-!
-Finally we can try out the widget.
--/
-
-#widget checkWidget .null
-
-/-!
-![`#check` as a service](../images/widgets_caas.png)
-
-## Building widget sources
-
-While typing JavaScript inline is fine for a simple example, for real developments we want to use
-packages from NPM, a proper build system, and JSX. Thus, most actual widget sources are built with
-Lake and NPM. They consist of multiple files and may import libraries which don't work as ESModules
-by default. On the other hand a widget source must be a single, self-contained ESModule in the form
-of a string. Readers familiar with web development may already have guessed that to obtain such a
-string, we need a *bundler*. Two popular choices are [`rollup.js`](https://rollupjs.org/guide/en/)
-and [`esbuild`](https://esbuild.github.io/). If we go with `rollup.js`, to make a widget work with
-the infoview we need to:
-- Set [`output.format`](https://rollupjs.org/guide/en/#outputformat) to `'es'`.
-- [Externalize](https://rollupjs.org/guide/en/#external) `react`, `react-dom`, `@leanprover/infoview`.
-  These libraries are already loaded by the infoview so they should not be bundled.
-
-In the RubiksCube sample, we provide a working `rollup.js` build configuration in
-[rollup.config.js](https://github.com/leanprover/lean4-samples/blob/main/RubiksCube/widget/rollup.config.js).
-
-## Inserting text
-
-We can also instruct the editor to insert text, copy text to the clipboard, or
-reveal a certain location in the document.
-To do this, use the `React.useContext(EditorContext)` React context.
-This will return an `EditorConnection` whose `api` field contains a number of methods to
-interact with the text editor.
-
-You can see the full API for this [here](https://github.com/leanprover/vscode-lean4/blob/master/lean4-infoview-api/src/infoviewApi.ts#L52)
--/
-
-@[widget]
-def insertTextWidget : UserWidgetDefinition where
-  name := "textInserter"
-  javascript := "
-import * as React from 'react';
-const e = React.createElement;
-import { EditorContext } from '@leanprover/infoview';
-
-export default function(props) {
-  const editorConnection = React.useContext(EditorContext)
-  function onClick() {
-    editorConnection.api.insertText('-- hello!!!', 'above')
-  }
-
-  return e('div', null, e('button', { value: name, onClick }, 'insert'))
-}
-"
-
-/-! Finally, we can try this out: -/
-
-#widget insertTextWidget .null

doc/examples/widgets.lean.md

@@ -1,5 +0,0 @@
-(this chapter is rendered by Alectryon in the CI)
-
-```lean
-{{#include widgets.lean}}
-```