chore: missing instances

cc @shigoel

.github/workflows/ci.yml

@@ -467,7 +467,6 @@ jobs:
         with:
           files: artifacts/*/*
           fail_on_unmatched_files: true
-          prerelease: ${{ !startsWith(github.ref, 'refs/tags/v') || contains(github.ref, '-rc') }}
         env:
           GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
 

flake.nix

@@ -35,28 +35,27 @@
       lean-packages = pkgs.callPackage (./nix/packages.nix) { src = ./.; inherit nix lean4-mode; };
 
       devShellWithDist = pkgsDist: pkgs.mkShell.override {
-          stdenv = pkgs.overrideCC pkgs.stdenv lean-packages.llvmPackages.clang;
-        } ({
-          buildInputs = with pkgs; [
-            cmake gmp ccache
-            lean-packages.llvmPackages.llvm  # llvm-symbolizer for asan/lsan
-            gdb
-            # TODO: only add when proven to not affect the flakification
-            #pkgs.python3
-            tree  # for CI
-          ];
-          # https://github.com/NixOS/nixpkgs/issues/60919
-          hardeningDisable = [ "all" ];
-          # more convenient `ctest` output
-          CTEST_OUTPUT_ON_FAILURE = 1;
-        } // pkgs.lib.optionalAttrs pkgs.stdenv.isLinux {
-          GMP = pkgsDist.gmp.override { withStatic = true; };
-          GLIBC = pkgsDist.glibc;
-          GLIBC_DEV = pkgsDist.glibc.dev;
-          GCC_LIB = pkgsDist.gcc.cc.lib;
-          ZLIB = pkgsDist.zlib;
-          GDB = pkgsDist.gdb;
-        });
+	  stdenv = pkgs.overrideCC pkgs.stdenv lean-packages.llvmPackages.clang;
+	} ({
+	  buildInputs = with pkgs; [
+	    cmake gmp ccache
+	    lean-packages.llvmPackages.llvm  # llvm-symbolizer for asan/lsan
+	    # TODO: only add when proven to not affect the flakification
+	    #pkgs.python3
+      tree  # for CI
+	  ];
+	  # https://github.com/NixOS/nixpkgs/issues/60919
+	  hardeningDisable = [ "all" ];
+	  # more convenient `ctest` output
+	  CTEST_OUTPUT_ON_FAILURE = 1;
+	} // pkgs.lib.optionalAttrs pkgs.stdenv.isLinux {
+	  GMP = pkgsDist.gmp.override { withStatic = true; };
+	  GLIBC = pkgsDist.glibc;
+	  GLIBC_DEV = pkgsDist.glibc.dev;
+	  GCC_LIB = pkgsDist.gcc.cc.lib;
+	  ZLIB = pkgsDist.zlib;
+	  GDB = pkgsDist.gdb;
+	});
     in {
       packages = lean-packages // rec {
         debug = lean-packages.override { debug = true; };

nix/bootstrap.nix

@@ -87,8 +87,7 @@ rec {
         leanFlags = [ "-DwarningAsError=true" ];
       } // args);
       Init' = build { name = "Init"; deps = []; };
-      Std' = build { name = "Std"; deps = [ Init' ]; };
-      Lean' = build { name = "Lean"; deps = [ Std' ]; };
+      Lean' = build { name = "Lean"; deps = [ Init' ]; };
       attachSharedLib = sharedLib: pkg: pkg // {
         inherit sharedLib;
         mods = mapAttrs (_: m: m // { inherit sharedLib; propagatedLoadDynlibs = []; }) pkg.mods;
@@ -96,8 +95,7 @@ rec {
     in (all: all // all.lean) rec {
       inherit (Lean) emacs-dev emacs-package vscode-dev vscode-package;
       Init = attachSharedLib leanshared Init';
-      Std = attachSharedLib leanshared Std' // { allExternalDeps = [ Init ]; };
-      Lean = attachSharedLib leanshared Lean' // { allExternalDeps = [ Std ]; };
+      Lean = attachSharedLib leanshared Lean' // { allExternalDeps = [ Init ]; };
       Lake = build {
         name = "Lake";
         src = src + "/src/lake";
@@ -111,22 +109,23 @@ rec {
         linkFlags = lib.optional stdenv.isLinux "-rdynamic";
         src = src + "/src/lake";
       };
-      stdlib = [ Init Std Lean Lake ];
+      stdlib = [ Init Lean Lake ];
       modDepsFiles = symlinkJoin { name = "modDepsFiles"; paths = map (l: l.modDepsFile) (stdlib ++ [ Leanc ]); };
       depRoots = symlinkJoin { name = "depRoots"; paths = map (l: l.depRoots) stdlib; };
       iTree = symlinkJoin { name = "ileans"; paths = map (l: l.iTree) stdlib; };
       Leanc = build { name = "Leanc"; src = lean-bin-tools-unwrapped.leanc_src; deps = stdlib; roots = [ "Leanc" ]; };
-      stdlibLinkFlags = "${lib.concatMapStringsSep " " (l: "-L${l.staticLib}") stdlib} -L${leancpp}/lib/lean";
+      stdlibLinkFlags = "-L${Init.staticLib} -L${Lean.staticLib} -L${Lake.staticLib} -L${leancpp}/lib/lean";
       libInit_shared = runCommand "libInit_shared" { buildInputs = [ stdenv.cc ]; libName = "libInit_shared${stdenv.hostPlatform.extensions.sharedLibrary}"; } ''
         mkdir $out
-        touch empty.c
-        ${stdenv.cc}/bin/cc -shared -o $out/$libName empty.c
+        LEAN_CC=${stdenv.cc}/bin/cc ${lean-bin-tools-unwrapped}/bin/leanc -shared -Wl,-Bsymbolic \
+          -Wl,--whole-archive -lInit ${leancpp}/lib/libleanrt_initial-exec.a -Wl,--no-whole-archive -lstdc++ -lm ${stdlibLinkFlags} \
+          $(${llvmPackages.libllvm.dev}/bin/llvm-config --ldflags --libs) \
+          -o $out/$libName
       '';
       leanshared = runCommand "leanshared" { buildInputs = [ stdenv.cc ]; libName = "libleanshared${stdenv.hostPlatform.extensions.sharedLibrary}"; } ''
         mkdir $out
-        LEAN_CC=${stdenv.cc}/bin/cc ${lean-bin-tools-unwrapped}/bin/leanc -shared ${lib.optionalString stdenv.isLinux "-Wl,-Bsymbolic"} \
-          ${if stdenv.isDarwin then "-Wl,-force_load,${Init.staticLib}/libInit.a -Wl,-force_load,${Lean.staticLib}/libStd.a -Wl,-force_load,${Lean.staticLib}/libLean.a -Wl,-force_load,${leancpp}/lib/lean/libleancpp.a ${leancpp}/lib/libleanrt_initial-exec.a -lc++"
-            else "-Wl,--whole-archive -lInit -lStd -lLean -lleancpp ${leancpp}/lib/libleanrt_initial-exec.a -Wl,--no-whole-archive -lstdc++"} -lm ${stdlibLinkFlags} \
+        LEAN_CC=${stdenv.cc}/bin/cc ${lean-bin-tools-unwrapped}/bin/leanc -shared -Wl,-Bsymbolic \
+          ${libInit_shared}/* -Wl,--whole-archive -lLean -lleancpp -Wl,--no-whole-archive -lstdc++ -lm ${stdlibLinkFlags} \
           $(${llvmPackages.libllvm.dev}/bin/llvm-config --ldflags --libs) \
           -o $out/$libName
       '';
@@ -152,9 +151,11 @@ rec {
         '';
         meta.mainProgram = "lean";
       };
-      cacheRoots = linkFarmFromDrvs "cacheRoots" ([
+      cacheRoots = linkFarmFromDrvs "cacheRoots" [
         stage0 lean leanc lean-all iTree modDepsFiles depRoots Leanc.src
-      ] ++ map (lib: lib.oTree) stdlib);
+        # .o files are not a runtime dependency on macOS because of lack of thin archives
+        Lean.oTree Lake.oTree
+      ];
       test = buildCMake {
         name = "lean-test-${desc}";
         realSrc = lib.sourceByRegex src [ "src.*" "tests.*" ];
@@ -177,7 +178,7 @@ rec {
         '';
       };
       update-stage0 =
-        let cTree = symlinkJoin { name = "cs"; paths = map (lib: lib.cTree) stdlib; }; in
+        let cTree = symlinkJoin { name = "cs"; paths = [ Init.cTree Lean.cTree Lake.cTree ]; }; in
         writeShellScriptBin "update-stage0" ''
           CSRCS=${cTree} CP_C_PARAMS="--dereference --no-preserve=all" ${src + "/script/lib/update-stage0"}
         '';

nix/buildLeanPackage.nix

@@ -5,7 +5,7 @@ let lean-final' = lean-final; in
 lib.makeOverridable (
 { name, src, fullSrc ? src, srcPrefix ? "", srcPath ? "$PWD/${srcPrefix}",
   # Lean dependencies. Each entry should be an output of buildLeanPackage.
-  deps ? [ lean.Init lean.Std lean.Lean ],
+  deps ? [ lean.Lean ],
   # Static library dependencies. Each derivation `static` should contain a static library in the directory `${static}`.
   staticLibDeps ? [],
   # Whether to wrap static library inputs in a -Wl,--start-group [...] -Wl,--end-group to ensure dependencies are resolved.
@@ -249,7 +249,7 @@ in rec {
     ${if stdenv.isDarwin then "-Wl,-force_load,${staticLib}/lib${libName}.a" else "-Wl,--whole-archive ${staticLib}/lib${libName}.a -Wl,--no-whole-archive"} \
     ${lib.concatStringsSep " " (map (d: "${d.sharedLib}/*") deps)}'';
   executable = lib.makeOverridable ({ withSharedStdlib ? true }: let
-      objPaths = map (drv: "${drv}/${drv.oPath}") (attrValues objects) ++ lib.optional withSharedStdlib "${lean-final.leanshared}/*";
+      objPaths = map (drv: "${drv}/${drv.oPath}") (attrValues objects) ++ lib.optional withSharedStdlib "${lean-final.libInit_shared}/* ${lean-final.leanshared}/*";
     in runCommand executableName { buildInputs = [ stdenv.cc leanc ]; } ''
       mkdir -p $out/bin
       leanc ${staticLibLinkWrapper (lib.concatStringsSep " " (objPaths ++ map (d: "${d}/*.a") allStaticLibDeps))} \

src/CMakeLists.txt

@@ -313,7 +313,7 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
   set(LEAN_CXX_STDLIB "-lc++")
 endif()
 
-string(APPEND TOOLCHAIN_STATIC_LINKER_FLAGS " ${LEAN_CXX_STDLIB} -lStd")
+string(APPEND TOOLCHAIN_STATIC_LINKER_FLAGS " ${LEAN_CXX_STDLIB}")
 string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " ${LEAN_CXX_STDLIB}")
 
 # in local builds, link executables and not just dynlibs against C++ stdlib as well,
@@ -514,11 +514,11 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
 endif()
 
 if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
-  set(LEANSHARED_LINKER_FLAGS "-Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libInit.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libStd.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libLean.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libleancpp.a ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS}")
+  set(LEANSHARED_LINKER_FLAGS "-Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libInit.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libLean.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libleancpp.a ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS}")
 elseif(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
-  set(LEANSHARED_LINKER_FLAGS "-Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/temp/libStd.a.export ${CMAKE_BINARY_DIR}/lib/temp/libLean.a.export -lleancpp -Wl,--no-whole-archive -lInit_shared -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libleanshared.dll.a")
+  set(LEANSHARED_LINKER_FLAGS "-Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/temp/libLean.a.export -lleancpp -Wl,--no-whole-archive -lInit_shared -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libleanshared.dll.a")
 else()
-  set(LEANSHARED_LINKER_FLAGS "-Wl,--whole-archive -lInit -lStd -lLean -lleancpp -Wl,--no-whole-archive ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS}")
+  set(LEANSHARED_LINKER_FLAGS "-Wl,--whole-archive -lInit -lLean -lleancpp -Wl,--no-whole-archive ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS}")
 endif()
 
 if (${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
@@ -540,7 +540,7 @@ add_custom_target(make_stdlib ALL
   # The actual rule is in a separate makefile because we want to prefix it with '+' to use the Make job server
   # for a parallelized nested build, but CMake doesn't let us do that.
   # We use `lean` from the previous stage, but `leanc`, headers, etc. from the current stage
-  COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make Init Std Lean
+  COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make Init Lean
   VERBATIM)
 
 # if we have LLVM enabled, then build `lean.h.bc` which has the LLVM bitcode

src/Init/Control/Except.lean

@@ -131,7 +131,7 @@ protected def adapt {ε' α : Type u} (f : ε → ε') : ExceptT ε m α → Exc
 end ExceptT
 
 @[always_inline]
-instance (m : Type u → Type v) (ε₁ : Type u) (ε₂ : Type u) [MonadExceptOf ε₁ m] : MonadExceptOf ε₁ (ExceptT ε₂ m) where
+instance (m : Type u → Type v) (ε₁ : Type u) (ε₂ : Type u) [Monad m] [MonadExceptOf ε₁ m] : MonadExceptOf ε₁ (ExceptT ε₂ m) where
   throw e := ExceptT.mk <| throwThe ε₁ e
   tryCatch x handle := ExceptT.mk <| tryCatchThe ε₁ x handle
 

src/Init/Control/Lawful/Basic.lean

@@ -9,7 +9,7 @@ import Init.Meta
 
 open Function
 
-@[simp] theorem monadLift_self {m : Type u → Type v} (x : m α) : monadLift x = x :=
+@[simp] theorem monadLift_self [Monad m] (x : m α) : monadLift x = x :=
   rfl
 
 /--

src/Init/Control/Lawful/Instances.lean

@@ -14,7 +14,7 @@ open Function
 
 namespace ExceptT
 
-theorem ext {x y : ExceptT ε m α} (h : x.run = y.run) : x = y := by
+theorem ext [Monad m] {x y : ExceptT ε m α} (h : x.run = y.run) : x = y := by
   simp [run] at h
   assumption
 
@@ -50,7 +50,7 @@ theorem run_bind [Monad m] (x : ExceptT ε m α)
 protected theorem seq_eq {α β ε : Type u} [Monad m] (mf : ExceptT ε m (α → β)) (x : ExceptT ε m α) : mf <*> x = mf >>= fun f => f <$> x :=
   rfl
 
-protected theorem bind_pure_comp [Monad m] (f : α → β) (x : ExceptT ε m α) : x >>= pure ∘ f = f <$> x := by
+protected theorem bind_pure_comp [Monad m] [LawfulMonad m] (f : α → β) (x : ExceptT ε m α) : x >>= pure ∘ f = f <$> x := by
   intros; rfl
 
 protected theorem seqLeft_eq {α β ε : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] (x : ExceptT ε m α) (y : ExceptT ε m β) : x <* y = const β <$> x <*> y := by
@@ -200,11 +200,11 @@ theorem ext {x y : StateT σ m α} (h : ∀ s, x.run s = y.run s) : x = y :=
   show (f >>= fun g => g <$> x).run s = _
   simp
 
-@[simp] theorem run_seqRight [Monad m] (x : StateT σ m α) (y : StateT σ m β) (s : σ) : (x *> y).run s = (x.run s >>= fun p => y.run p.2) := by
+@[simp] theorem run_seqRight [Monad m] [LawfulMonad m] (x : StateT σ m α) (y : StateT σ m β) (s : σ) : (x *> y).run s = (x.run s >>= fun p => y.run p.2) := by
   show (x >>= fun _ => y).run s = _
   simp
 
-@[simp] theorem run_seqLeft {α β σ : Type u} [Monad m] (x : StateT σ m α) (y : StateT σ m β) (s : σ) : (x <* y).run s = (x.run s >>= fun p => y.run p.2 >>= fun p' => pure (p.1, p'.2)) := by
+@[simp] theorem run_seqLeft {α β σ : Type u} [Monad m] [LawfulMonad m] (x : StateT σ m α) (y : StateT σ m β) (s : σ) : (x <* y).run s = (x.run s >>= fun p => y.run p.2 >>= fun p' => pure (p.1, p'.2)) := by
   show (x >>= fun a => y >>= fun _ => pure a).run s = _
   simp
 

src/Init/Control/Option.lean

@@ -67,7 +67,7 @@ instance : MonadExceptOf Unit (OptionT m) where
   throw    := fun _ => OptionT.fail
   tryCatch := OptionT.tryCatch
 
-instance (ε : Type u) [MonadExceptOf ε m] : MonadExceptOf ε (OptionT m) where
+instance (ε : Type u) [Monad m] [MonadExceptOf ε m] : MonadExceptOf ε (OptionT m) where
   throw e           := OptionT.mk <| throwThe ε e
   tryCatch x handle := OptionT.mk <| tryCatchThe ε x handle
 

src/Init/Control/Reader.lean

@@ -32,7 +32,7 @@ instance : MonadControl m (ReaderT ρ m) where
   restoreM x _ := x
 
 @[always_inline]
-instance ReaderT.tryFinally [MonadFinally m] : MonadFinally (ReaderT ρ m) where
+instance ReaderT.tryFinally [MonadFinally m] [Monad m] : MonadFinally (ReaderT ρ m) where
   tryFinally' x h ctx := tryFinally' (x ctx) (fun a? => h a? ctx)
 
 @[reducible] def ReaderM (ρ : Type u) := ReaderT ρ Id

src/Init/Control/State.lean

@@ -87,7 +87,7 @@ protected def lift {α : Type u} (t : m α) : StateT σ m α :=
 instance : MonadLift m (StateT σ m) := ⟨StateT.lift⟩
 
 @[always_inline]
-instance (σ m) : MonadFunctor m (StateT σ m) := ⟨fun f x s => f (x s)⟩
+instance (σ m) [Monad m] : MonadFunctor m (StateT σ m) := ⟨fun f x s => f (x s)⟩
 
 @[always_inline]
 instance (ε) [MonadExceptOf ε m] : MonadExceptOf ε (StateT σ m) := {

src/Init/Control/StateCps.lean

@@ -14,18 +14,16 @@ def StateCpsT (σ : Type u) (m : Type u → Type v) (α : Type u) := (δ : Type
 
 namespace StateCpsT
 
-variable {α σ : Type u} {m : Type u → Type v}
-
 @[always_inline, inline]
-def runK (x : StateCpsT σ m α) (s : σ) (k : α → σ → m β) : m β :=
+def runK {α σ : Type u} {m : Type u → Type v}  (x : StateCpsT σ m α) (s : σ) (k : α → σ → m β) : m β :=
   x _ s k
 
 @[always_inline, inline]
-def run [Monad m] (x : StateCpsT σ m α) (s : σ) : m (α × σ) :=
+def run {α σ : Type u} {m : Type u → Type v} [Monad m] (x : StateCpsT σ m α) (s : σ) : m (α × σ) :=
   runK x s (fun a s => pure (a, s))
 
 @[always_inline, inline]
-def run' [Monad m] (x : StateCpsT σ m α) (s : σ) : m α :=
+def run' {α σ : Type u} {m : Type u → Type v}  [Monad m] (x : StateCpsT σ m α) (s : σ) : m α :=
   runK x s (fun a _ => pure a)
 
 @[always_inline]
@@ -50,29 +48,29 @@ protected def lift [Monad m] (x : m α) : StateCpsT σ m α :=
 instance [Monad m] : MonadLift m (StateCpsT σ m) where
   monadLift := StateCpsT.lift
 
-@[simp] theorem runK_pure (a : α) (s : σ) (k : α → σ → m β) : (pure a : StateCpsT σ m α).runK s k = k a s := rfl
+@[simp] theorem runK_pure {m : Type u → Type v} (a : α) (s : σ) (k : α → σ → m β) : (pure a : StateCpsT σ m α).runK s k = k a s := rfl
 
-@[simp] theorem runK_get (s : σ) (k : σ → σ → m β) : (get : StateCpsT σ m σ).runK s k = k s s := rfl
+@[simp] theorem runK_get {m : Type u → Type v} (s : σ) (k : σ → σ → m β) : (get : StateCpsT σ m σ).runK s k = k s s := rfl
 
-@[simp] theorem runK_set (s s' : σ) (k : PUnit → σ → m β) : (set s' : StateCpsT σ m PUnit).runK s k = k ⟨⟩ s' := rfl
+@[simp] theorem runK_set {m : Type u → Type v} (s s' : σ) (k : PUnit → σ → m β) : (set s' : StateCpsT σ m PUnit).runK s k = k ⟨⟩ s' := rfl
 
-@[simp] theorem runK_modify (f : σ → σ) (s : σ) (k : PUnit → σ → m β) : (modify f : StateCpsT σ m PUnit).runK s k = k ⟨⟩ (f s) := rfl
+@[simp] theorem runK_modify {m : Type u → Type v} (f : σ → σ) (s : σ) (k : PUnit → σ → m β) : (modify f : StateCpsT σ m PUnit).runK s k = k ⟨⟩ (f s) := rfl
 
-@[simp] theorem runK_lift [Monad m] (x : m α) (s : σ) (k : α → σ → m β) : (StateCpsT.lift x : StateCpsT σ m α).runK s k = x >>= (k . s) := rfl
+@[simp] theorem runK_lift {α σ : Type u} [Monad m] (x : m α) (s : σ) (k : α → σ → m β) : (StateCpsT.lift x : StateCpsT σ m α).runK s k = x >>= (k . s) := rfl
 
-@[simp] theorem runK_monadLift [Monad m] [MonadLiftT n m] (x : n α) (s : σ) (k : α → σ → m β)
+@[simp] theorem runK_monadLift {σ : Type u} [Monad m] [MonadLiftT n m] (x : n α) (s : σ) (k : α → σ → m β)
     : (monadLift x : StateCpsT σ m α).runK s k = (monadLift x : m α) >>= (k . s) := rfl
 
-@[simp] theorem runK_bind_pure (a : α) (f : α → StateCpsT σ m β) (s : σ) (k : β → σ → m γ) : (pure a >>= f).runK s k = (f a).runK s k := rfl
+@[simp] theorem runK_bind_pure {α σ : Type u} [Monad m] (a : α) (f : α → StateCpsT σ m β) (s : σ) (k : β → σ → m γ) : (pure a >>= f).runK s k = (f a).runK s k := rfl
 
-@[simp] theorem runK_bind_lift [Monad m] (x : m α) (f : α → StateCpsT σ m β) (s : σ) (k : β → σ → m γ)
+@[simp] theorem runK_bind_lift {α σ : Type u} [Monad m] (x : m α) (f : α → StateCpsT σ m β) (s : σ) (k : β → σ → m γ)
     : (StateCpsT.lift x >>= f).runK s k = x >>= fun a => (f a).runK s k := rfl
 
-@[simp] theorem runK_bind_get (f : σ → StateCpsT σ m β) (s : σ) (k : β → σ → m γ) : (get >>= f).runK s k = (f s).runK s k := rfl
+@[simp] theorem runK_bind_get {σ : Type u} [Monad m] (f : σ → StateCpsT σ m β) (s : σ) (k : β → σ → m γ) : (get >>= f).runK s k = (f s).runK s k := rfl
 
-@[simp] theorem runK_bind_set (f : PUnit → StateCpsT σ m β) (s s' : σ) (k : β → σ → m γ) : (set s' >>= f).runK s k = (f ⟨⟩).runK s' k := rfl
+@[simp] theorem runK_bind_set {σ : Type u} [Monad m] (f : PUnit → StateCpsT σ m β) (s s' : σ) (k : β → σ → m γ) : (set s' >>= f).runK s k = (f ⟨⟩).runK s' k := rfl
 
-@[simp] theorem runK_bind_modify (f : σ → σ) (g : PUnit → StateCpsT σ m β) (s : σ) (k : β → σ → m γ) : (modify f >>= g).runK s k = (g ⟨⟩).runK (f s) k := rfl
+@[simp] theorem runK_bind_modify {σ : Type u} [Monad m] (f : σ → σ) (g : PUnit → StateCpsT σ m β) (s : σ) (k : β → σ → m γ) : (modify f >>= g).runK s k = (g ⟨⟩).runK (f s) k := rfl
 
 @[simp] theorem run_eq [Monad m] (x : StateCpsT σ m α) (s : σ) : x.run s = x.runK s (fun a s => pure (a, s)) := rfl
 

src/Init/Control/StateRef.lean

@@ -34,22 +34,22 @@ protected def lift (x : m α) : StateRefT' ω σ m α :=
 
 instance [Monad m] : Monad (StateRefT' ω σ m) := inferInstanceAs (Monad (ReaderT _ _))
 instance : MonadLift m (StateRefT' ω σ m) := ⟨StateRefT'.lift⟩
-instance (σ m) : MonadFunctor m (StateRefT' ω σ m) := inferInstanceAs (MonadFunctor m (ReaderT _ _))
+instance (σ m) [Monad m] : MonadFunctor m (StateRefT' ω σ m) := inferInstanceAs (MonadFunctor m (ReaderT _ _))
 instance [Alternative m] [Monad m] : Alternative (StateRefT' ω σ m) := inferInstanceAs (Alternative (ReaderT _ _))
 
 @[inline]
-protected def get [MonadLiftT (ST ω) m] : StateRefT' ω σ m σ :=
+protected def get [Monad m] [MonadLiftT (ST ω) m] : StateRefT' ω σ m σ :=
   fun ref => ref.get
 
 @[inline]
-protected def set [MonadLiftT (ST ω) m] (s : σ) : StateRefT' ω σ m PUnit :=
+protected def set [Monad m] [MonadLiftT (ST ω) m] (s : σ) : StateRefT' ω σ m PUnit :=
   fun ref => ref.set s
 
 @[inline]
-protected def modifyGet [MonadLiftT (ST ω) m] (f : σ → α × σ) : StateRefT' ω σ m α :=
+protected def modifyGet [Monad m] [MonadLiftT (ST ω) m] (f : σ → α × σ) : StateRefT' ω σ m α :=
   fun ref => ref.modifyGet f
 
-instance [MonadLiftT (ST ω) m] : MonadStateOf σ (StateRefT' ω σ m) where
+instance [MonadLiftT (ST ω) m] [Monad m] : MonadStateOf σ (StateRefT' ω σ m) where
   get       := StateRefT'.get
   set       := StateRefT'.set
   modifyGet := StateRefT'.modifyGet

src/Init/Core.lean

@@ -642,7 +642,7 @@ instance : LawfulBEq String := inferInstance
 
 /-! # Logical connectives and equality -/
 
-@[inherit_doc True.intro] theorem trivial : True := ⟨⟩
+@[inherit_doc True.intro] def trivial : True := ⟨⟩
 
 theorem mt {a b : Prop} (h₁ : a → b) (h₂ : ¬b) : ¬a :=
   fun ha => h₂ (h₁ ha)
@@ -1173,7 +1173,7 @@ def Prod.lexLt [LT α] [LT β] (s : α × β) (t : α × β) : Prop :=
   s.1 < t.1 ∨ (s.1 = t.1 ∧ s.2 < t.2)
 
 instance Prod.lexLtDec
-    [LT α] [LT β] [DecidableEq α]
+    [LT α] [LT β] [DecidableEq α] [DecidableEq β]
     [(a b : α) → Decidable (a < b)] [(a b : β) → Decidable (a < b)]
     : (s t : α × β) → Decidable (Prod.lexLt s t) :=
   fun _ _ => inferInstanceAs (Decidable (_ ∨ _))
@@ -1191,11 +1191,6 @@ def Prod.map {α₁ : Type u₁} {α₂ : Type u₂} {β₁ : Type v₁} {β₂
     (f : α₁ → α₂) (g : β₁ → β₂) : α₁ × β₁ → α₂ × β₂
   | (a, b) => (f a, g b)
 
-@[simp] theorem Prod.map_apply (f : α → β) (g : γ → δ) (x) (y) :
-    Prod.map f g (x, y) = (f x, g y) := rfl
-@[simp] theorem Prod.map_fst (f : α → β) (g : γ → δ) (x) : (Prod.map f g x).1 = f x.1 := rfl
-@[simp] theorem Prod.map_snd (f : α → β) (g : γ → δ) (x) : (Prod.map f g x).2 = g x.2 := rfl
-
 /-! # Dependent products -/
 
 theorem ex_of_PSigma {α : Type u} {p : α → Prop} : (PSigma (fun x => p x)) → Exists (fun x => p x)

src/Init/Data/Array/Basic.lean

@@ -60,6 +60,8 @@ def uget (a : @& Array α) (i : USize) (h : i.toNat < a.size) : α :=
 instance : GetElem (Array α) USize α fun xs i => i.toNat < xs.size where
   getElem xs i h := xs.uget i h
 
+instance : LawfulGetElem (Array α) USize α fun xs i => i.toNat < xs.size where
+
 def back [Inhabited α] (a : Array α) : α :=
   a.get! (a.size - 1)
 

src/Init/Data/Array/Lemmas.lean

@@ -220,7 +220,7 @@ theorem getElem?_len_le (a : Array α) {i : Nat} (h : a.size ≤ i) : a[i]? = no
 theorem getD_get? (a : Array α) (i : Nat) (d : α) :
   Option.getD a[i]? d = if p : i < a.size then a[i]'p else d := by
   if h : i < a.size then
-    simp [setD, h, getElem?_def]
+    simp [setD, h, getElem?]
   else
     have p : i ≥ a.size := Nat.le_of_not_gt h
     simp [setD, getElem?_len_le _ p, h]
@@ -383,18 +383,18 @@ theorem get?_push {a : Array α} : (a.push x)[i]? = if i = a.size then some x el
   | Or.inl g =>
     have h1 : i < a.size + 1 := by omega
     have h2 : i ≠ a.size := by omega
-    simp [getElem?_def, size_push, g, h1, h2, get_push_lt]
+    simp [getElem?, size_push, g, h1, h2, get_push_lt]
   | Or.inr (Or.inl heq) =>
     simp [heq, getElem?_pos, get_push_eq]
   | Or.inr (Or.inr g) =>
-    simp only [getElem?_def, size_push]
+    simp only [getElem?, size_push]
     have h1 : ¬ (i < a.size) := by omega
     have h2 : ¬ (i < a.size + 1) := by omega
     have h3 : i ≠ a.size := by omega
     simp [h1, h2, h3]
 
 @[simp] theorem get?_size {a : Array α} : a[a.size]? = none := by
-  simp only [getElem?_def, Nat.lt_irrefl, dite_false]
+  simp only [getElem?, Nat.lt_irrefl, dite_false]
 
 @[simp] theorem data_set (a : Array α) (i v) : (a.set i v).data = a.data.set i.1 v := rfl
 
@@ -750,7 +750,7 @@ theorem mem_of_mem_filter {a : α} {l} (h : a ∈ filter p l) : a ∈ l :=
   exact this #[]
   induction l
   · simp_all [Id.run]
-  · simp_all [Id.run, List.filterMap_cons]
+  · simp_all [Id.run]
     split <;> simp_all
 
 @[simp] theorem mem_filterMap (f : α → Option β) (l : Array α) {b : β} :

src/Init/Data/Array/Subarray.lean

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

src/Init/Data/BitVec/Basic.lean

@@ -614,13 +614,6 @@ theorem ofBool_append (msb : Bool) (lsbs : BitVec w) :
     ofBool msb ++ lsbs = (cons msb lsbs).cast (Nat.add_comm ..) :=
   rfl
 
-/--
-`twoPow w i` is the bitvector `2^i` if `i < w`, and `0` otherwise.
-That is, 2 to the power `i`.
-For the bitwise point of view, it has the `i`th bit as `1` and all other bits as `0`.
--/
-def twoPow (w : Nat) (i : Nat) : BitVec w := 1#w <<< i
-
 end bitwise
 
 section normalization_eqs

src/Init/Data/BitVec/Lemmas.lean

@@ -184,7 +184,8 @@ theorem msb_eq_getLsb_last (x : BitVec w) :
     · simp only [h]
       rw [Nat.div_eq_sub_div (Nat.two_pow_pos w) h, Nat.div_eq_of_lt]
       · decide
-      · omega
+      · have : BitVec.toNat x < 2^w + 2^w := by simpa [Nat.pow_succ, Nat.mul_two] using x.isLt
+        omega
 
 @[bv_toNat] theorem getLsb_succ_last (x : BitVec (w + 1)) :
     x.getLsb w = decide (2 ^ w ≤ x.toNat) := getLsb_last x
@@ -330,7 +331,10 @@ theorem toNat_eq_nat (x : BitVec w) (y : Nat)
   : (x.toNat = y) ↔ (y < 2^w ∧ (x = BitVec.ofNat w y)) := by
   apply Iff.intro
   · intro eq
-    simp [←eq, x.isLt]
+    simp at eq
+    have lt := x.isLt
+    simp [eq] at lt
+    simp [←eq, lt, x.isLt]
   · intro eq
     simp [Nat.mod_eq_of_lt, eq]
 
@@ -1236,7 +1240,11 @@ x.rotateLeft 2 = (<6 5 | 4 3 2 1 0>).rotateLeft 2 = <3 2 1 0 | 6 5>
 theorem getLsb_rotateLeftAux_of_le {x : BitVec w} {r : Nat} {i : Nat} (hi : i < r) :
     (x.rotateLeftAux r).getLsb i = x.getLsb (w - r + i) := by
   rw [rotateLeftAux, getLsb_or, getLsb_ushiftRight]
-  simp; omega
+  suffices (x <<< r).getLsb i = false by
+    simp; omega
+  simp only [getLsb_shiftLeft, Bool.and_eq_false_imp, Bool.and_eq_true, decide_eq_true_eq,
+    Bool.not_eq_true', decide_eq_false_iff_not, Nat.not_lt, and_imp]
+  omega
 
 /--
 Accessing bits in `x.rotateLeft r` the range `[r, w)` is equal to
@@ -1367,51 +1375,4 @@ theorem getLsb_rotateRight {x : BitVec w} {r i : Nat} :
   · simp
   · rw [← rotateRight_mod_eq_rotateRight, getLsb_rotateRight_of_le (Nat.mod_lt _ (by omega))]
 
-/- ## twoPow -/
-
-@[simp, bv_toNat]
-theorem toNat_twoPow (w : Nat) (i : Nat) : (twoPow w i).toNat = 2^i % 2^w := by
-  rcases w with rfl | w
-  · simp [Nat.mod_one]
-  · simp only [twoPow, toNat_shiftLeft, toNat_ofNat]
-    have h1 : 1 < 2 ^ (w + 1) := Nat.one_lt_two_pow (by omega)
-    rw [Nat.mod_eq_of_lt h1, Nat.shiftLeft_eq, Nat.one_mul]
-
-@[simp]
-theorem getLsb_twoPow (i j : Nat) : (twoPow w i).getLsb j = ((i < w) && (i = j)) := by
-  rcases w with rfl | w
-  · simp; omega
-  · simp only [twoPow, getLsb_shiftLeft, getLsb_ofNat]
-    by_cases hj : j < i
-    · simp only [hj, decide_True, Bool.not_true, Bool.and_false, Bool.false_and, Bool.false_eq,
-      Bool.and_eq_false_imp, decide_eq_true_eq, decide_eq_false_iff_not]
-      omega
-    · by_cases hi : Nat.testBit 1 (j - i)
-      · obtain hi' := Nat.testBit_one_eq_true_iff_self_eq_zero.mp hi
-        have hij : j = i := by omega
-        simp_all
-      · have hij : i ≠ j := by
-          intro h; subst h
-          simp at hi
-        simp_all
-
-theorem and_twoPow_eq (x : BitVec w) (i : Nat) :
-    x &&& (twoPow w i) = if x.getLsb i then twoPow w i else 0#w := by
-  ext j
-  simp only [getLsb_and, getLsb_twoPow]
-  by_cases hj : i = j <;> by_cases hx : x.getLsb i <;> simp_all
-
-@[simp]
-theorem mul_twoPow_eq_shiftLeft (x : BitVec w) (i : Nat) :
-    x * (twoPow w i) = x <<< i := by
-  apply eq_of_toNat_eq
-  simp only [toNat_mul, toNat_twoPow, toNat_shiftLeft, Nat.shiftLeft_eq]
-  by_cases hi : i < w
-  · have hpow : 2^i < 2^w := Nat.pow_lt_pow_of_lt (by omega) (by omega)
-    rw [Nat.mod_eq_of_lt hpow]
-  · have hpow : 2 ^ i % 2 ^ w = 0 := by
-      rw [Nat.mod_eq_zero_of_dvd]
-      apply Nat.pow_dvd_pow 2 (by omega)
-    simp [Nat.mul_mod, hpow]
-
 end BitVec

src/Init/Data/ByteArray/Basic.lean

@@ -52,9 +52,13 @@ def get : (a : @& ByteArray) → (@& Fin a.size) → UInt8
 instance : GetElem ByteArray Nat UInt8 fun xs i => i < xs.size where
   getElem xs i h := xs.get ⟨i, h⟩
 
+instance : LawfulGetElem ByteArray Nat UInt8 fun xs i => i < xs.size where
+
 instance : GetElem ByteArray USize UInt8 fun xs i => i.val < xs.size where
   getElem xs i h := xs.uget i h
 
+instance : LawfulGetElem ByteArray USize UInt8 fun xs i => i.val < xs.size where
+
 @[extern "lean_byte_array_set"]
 def set! : ByteArray → (@& Nat) → UInt8 → ByteArray
   | ⟨bs⟩, i, b => ⟨bs.set! i b⟩

src/Init/Data/Fin/Lemmas.lean

@@ -378,7 +378,7 @@ theorem castSucc_lt_succ (i : Fin n) : Fin.castSucc i < i.succ :=
   lt_def.2 <| by simp only [coe_castSucc, val_succ, Nat.lt_succ_self]
 
 theorem le_castSucc_iff {i : Fin (n + 1)} {j : Fin n} : i ≤ Fin.castSucc j ↔ i < j.succ := by
-  simpa only [lt_def, le_def] using Nat.add_one_le_add_one_iff.symm
+  simpa [lt_def, le_def] using Nat.succ_le_succ_iff.symm
 
 theorem castSucc_lt_iff_succ_le {n : Nat} {i : Fin n} {j : Fin (n + 1)} :
     Fin.castSucc i < j ↔ i.succ ≤ j := .rfl

src/Init/Data/FloatArray/Basic.lean

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

src/Init/Data/Int/DivModLemmas.lean

@@ -636,7 +636,7 @@ theorem sub_ediv_of_dvd (a : Int) {b c : Int}
   have := Int.mul_ediv_cancel 1 H; rwa [Int.one_mul] at this
 
 @[simp]
-theorem emod_sub_cancel (x y : Int): (x - y)%y = x%y := by
+theorem Int.emod_sub_cancel (x y : Int): (x - y)%y = x%y := by
   by_cases h : y = 0
   · simp [h]
   · simp only [Int.emod_def, Int.sub_ediv_of_dvd, Int.dvd_refl, Int.ediv_self h, Int.mul_sub]

src/Init/Data/Int/Order.lean

@@ -127,14 +127,9 @@ protected theorem lt_iff_le_not_le {a b : Int} : a < b ↔ a ≤ b ∧ ¬b ≤ a
   · exact Int.le_antisymm h h'
   · subst h'; apply Int.le_refl
 
-protected theorem lt_of_not_ge {a b : Int} (h : ¬a ≤ b) : b < a :=
-  Int.lt_iff_le_not_le.mpr ⟨(Int.le_total ..).resolve_right h, h⟩
-
-protected theorem not_le_of_gt {a b : Int} (h : b < a) : ¬a ≤ b :=
-  (Int.lt_iff_le_not_le.mp h).right
-
 protected theorem not_le {a b : Int} : ¬a ≤ b ↔ b < a :=
-  Iff.intro Int.lt_of_not_ge Int.not_le_of_gt
+  ⟨fun h => Int.lt_iff_le_not_le.2 ⟨(Int.le_total ..).resolve_right h, h⟩,
+   fun h => (Int.lt_iff_le_not_le.1 h).2⟩
 
 protected theorem not_lt {a b : Int} : ¬a < b ↔ b ≤ a :=
   by rw [← Int.not_le, Decidable.not_not]
@@ -514,6 +509,9 @@ theorem mem_toNat' : ∀ (a : Int) (n : Nat), toNat' a = some n ↔ a = n
 
 /-! ## Order properties of the integers -/
 
+protected theorem lt_of_not_ge {a b : Int} : ¬a ≤ b → b < a := Int.not_le.mp
+protected theorem not_le_of_gt {a b : Int} : b < a → ¬a ≤ b := Int.not_le.mpr
+
 protected theorem le_of_not_le {a b : Int} : ¬ a ≤ b → b ≤ a := (Int.le_total a b).resolve_left
 
 @[simp] theorem negSucc_not_pos (n : Nat) : 0 < -[n+1] ↔ False := by
@@ -588,10 +586,7 @@ theorem add_one_le_iff {a b : Int} : a + 1 ≤ b ↔ a < b := .rfl
 theorem lt_add_one_iff {a b : Int} : a < b + 1 ↔ a ≤ b := Int.add_le_add_iff_right _
 
 @[simp] theorem succ_ofNat_pos (n : Nat) : 0 < (n : Int) + 1 :=
-  lt_add_one_iff.mpr (ofNat_zero_le _)
-
-theorem not_ofNat_neg (n : Nat) : ¬((n : Int) < 0) :=
-  Int.not_lt.mpr (ofNat_zero_le ..)
+  lt_add_one_iff.2 (ofNat_zero_le _)
 
 theorem le_add_one {a b : Int} (h : a ≤ b) : a ≤ b + 1 :=
   Int.le_of_lt (Int.lt_add_one_iff.2 h)
@@ -806,12 +801,6 @@ protected theorem lt_add_of_neg_lt_sub_right {a b c : Int} (h : -b < a - c) : c
 protected theorem neg_lt_sub_right_of_lt_add {a b c : Int} (h : c < a + b) : -b < a - c :=
   Int.lt_sub_left_of_add_lt (Int.sub_right_lt_of_lt_add h)
 
-protected theorem add_lt_iff (a b c : Int) : a + b < c ↔ a < -b + c := by
-  rw [← Int.add_lt_add_iff_left (-b), Int.add_comm (-b), Int.add_neg_cancel_right]
-
-protected theorem sub_lt_iff (a b c : Int) : a - b < c ↔ a < c + b :=
-  Iff.intro Int.lt_add_of_sub_right_lt Int.sub_right_lt_of_lt_add
-
 protected theorem sub_lt_of_sub_lt {a b c : Int} (h : a - b < c) : a - c < b :=
   Int.sub_left_lt_of_lt_add (Int.lt_add_of_sub_right_lt h)
 

src/Init/Data/List/Basic.lean

@@ -67,9 +67,6 @@ namespace List
 
 @[simp 1100] theorem length_singleton (a : α) : length [a] = 1 := rfl
 
-@[simp] theorem length_cons {α} (a : α) (as : List α) : (cons a as).length = as.length + 1 :=
-  rfl
-
 /-! ### set -/
 
 @[simp] theorem length_set (as : List α) (i : Nat) (a : α) : (as.set i a).length = as.length := by
@@ -401,7 +398,7 @@ filterMap
     | some b => b :: filterMap f as
 
 @[simp] theorem filterMap_nil (f : α → Option β) : filterMap f [] = [] := rfl
-theorem filterMap_cons (f : α → Option β) (a : α) (l : List α) :
+@[simp] theorem filterMap_cons (f : α → Option β) (a : α) (l : List α) :
     filterMap f (a :: l) =
       match f a with
       | none => filterMap f l
@@ -565,17 +562,12 @@ set_option linter.missingDocs false in
 `replicate n a` is `n` copies of `a`:
 * `replicate 5 a = [a, a, a, a, a]`
 -/
-def replicate : (n : Nat) → (a : α) → List α
+@[simp] def replicate : (n : Nat) → (a : α) → List α
   | 0,   _ => []
   | n+1, a => a :: replicate n a
 
-@[simp] theorem replicate_zero : replicate 0 a = [] := rfl
-theorem replicate_succ (a : α) (n) : replicate (n+1) a = a :: replicate n a := rfl
-
 @[simp] theorem length_replicate (n : Nat) (a : α) : (replicate n a).length = n := by
-  induction n with
-  | zero => simp
-  | succ n ih => simp only [ih, replicate_succ, length_cons, Nat.succ_eq_add_one]
+  induction n <;> simp_all
 
 /-! ## List membership
 
@@ -614,13 +606,13 @@ def isEmpty : List α → Bool
 -/
 def elem [BEq α] (a : α) : List α → Bool
   | []    => false
-  | b::bs => match a == b with
+  | b::bs => match b == a with
     | true  => true
     | false => elem a bs
 
 @[simp] theorem elem_nil [BEq α] : ([] : List α).elem a = false := rfl
 theorem elem_cons [BEq α] {a : α} :
-    (b::bs).elem a = match a == b with | true => true | false => bs.elem a := rfl
+    (a::as).elem b = match a == b with | true => true | false => as.elem b := rfl
 
 /-- `notElem a l` is `!(elem a l)`. -/
 @[deprecated (since := "2024-06-15")]
@@ -743,7 +735,7 @@ theorem drop_eq_nil_of_le {as : List α} {i : Nat} (h : as.length ≤ i) : as.dr
   match as, i with
   | [],    i   => simp
   | _::_,  0   => simp at h
-  | _::as, i+1 => simp only [length_cons] at h; exact @drop_eq_nil_of_le as i (Nat.le_of_succ_le_succ h)
+  | _::as, i+1 => simp at h; exact @drop_eq_nil_of_le as i (Nat.le_of_succ_le_succ h)
 
 /-! ### takeWhile -/
 
@@ -855,9 +847,6 @@ That is, there exists a `t` such that `l₂ == t ++ l₁`. -/
 def isSuffixOf [BEq α] (l₁ l₂ : List α) : Bool :=
   isPrefixOf l₁.reverse l₂.reverse
 
-@[simp] theorem isSuffixOf_nil_left [BEq α] : isSuffixOf ([] : List α) l = true := by
-  simp [isSuffixOf]
-
 /-! ### isSuffixOf? -/
 
 /-- `isSuffixOf? l₁ l₂` returns `some t` when `l₂ == t ++ l₁`.-/
@@ -883,8 +872,6 @@ def rotateLeft (xs : List α) (n : Nat := 1) : List α :=
     let e := xs.drop n
     e ++ b
 
-@[simp] theorem rotateLeft_nil : ([] : List α).rotateLeft n = [] := rfl
-
 /-! ### rotateRight -/
 
 /--
@@ -904,8 +891,6 @@ def rotateRight (xs : List α) (n : Nat := 1) : List α :=
     let e := xs.drop n
     e ++ b
 
-@[simp] theorem rotateRight_nil : ([] : List α).rotateRight n = [] := rfl
-
 /-! ## Manipulating elements -/
 
 /-! ### replace -/
@@ -918,13 +903,13 @@ def rotateRight (xs : List α) (n : Nat := 1) : List α :=
 -/
 def replace [BEq α] : List α → α → α → List α
   | [],    _, _ => []
-  | a::as, b, c => match b == a with
+  | a::as, b, c => match a == b with
     | true  => c::as
     | false => a :: replace as b c
 
 @[simp] theorem replace_nil [BEq α] : ([] : List α).replace a b = [] := rfl
 theorem replace_cons [BEq α] {a : α} :
-    (a::as).replace b c = match b == a with | true => c::as | false => a :: replace as b c :=
+    (a::as).replace b c = match a == b with | true => c::as | false => a :: replace as b c :=
   rfl
 
 /-! ### insert -/

src/Init/Data/List/Impl.lean

@@ -258,7 +258,7 @@ theorem replicateTR_loop_eq : ∀ n, replicateTR.loop a n acc = replicate n a ++
   unless `b` is not found in `xs` in which case it returns `l`. -/
   @[specialize] go : List α → Array α → List α
   | [], _ => l
-  | a::as, acc => bif b == a then acc.toListAppend (c::as) else go as (acc.push a)
+  | a::as, acc => bif a == b then acc.toListAppend (c::as) else go as (acc.push a)
 
 @[csimp] theorem replace_eq_replaceTR : @List.replace = @replaceTR := by
   funext α _ l b c; simp [replaceTR]

src/Init/Data/List/TakeDrop.lean

@@ -39,15 +39,10 @@ theorem take_take : ∀ (n m) (l : List α), take n (take m l) = take (min n m)
   | succ n, succ m, a :: l => by
     simp only [take, succ_min_succ, take_take n m l]
 
-@[simp] theorem take_replicate (a : α) : ∀ n m : Nat, take n (replicate m a) = replicate (min n m) a
+theorem take_replicate (a : α) : ∀ n m : Nat, take n (replicate m a) = replicate (min n m) a
   | n, 0 => by simp [Nat.min_zero]
   | 0, m => by simp [Nat.zero_min]
-  | succ n, succ m => by simp [replicate_succ, succ_min_succ, take_replicate]
-
-@[simp] theorem drop_replicate (a : α) : ∀ n m : Nat, drop n (replicate m a) = replicate (m - n) a
-  | n, 0 => by simp
-  | 0, m => by simp
-  | succ n, succ m => by simp [replicate_succ, succ_sub_succ, drop_replicate]
+  | succ n, succ m => by simp [succ_min_succ, take_replicate]
 
 /-- Taking the first `n` elements in `l₁ ++ l₂` is the same as appending the first `n` elements
 of `l₁` to the first `n - l₁.length` elements of `l₂`. -/
@@ -102,7 +97,7 @@ theorem get_take' (L : List α) {j i} :
 
 theorem getElem?_take_eq_none {l : List α} {n m : Nat} (h : n ≤ m) :
     (l.take n)[m]? = none :=
-  getElem?_eq_none <| Nat.le_trans (length_take_le _ _) h
+  getElem?_eq_none.mpr <| Nat.le_trans (length_take_le _ _) h
 
 @[deprecated getElem?_take_eq_none (since := "2024-06-12")]
 theorem get?_take_eq_none {l : List α} {n m : Nat} (h : n ≤ m) :
@@ -303,32 +298,6 @@ theorem take_reverse {α} {xs : List α} (n : Nat) (h : n ≤ xs.length) :
 
 @[deprecated (since := "2024-06-15")] abbrev reverse_take := @take_reverse
 
-/-! ### rotateLeft -/
-
-@[simp] theorem rotateLeft_replicate (n) (a : α) : rotateLeft (replicate m a) n = replicate m a := by
-  cases n with
-  | zero => simp
-  | succ n =>
-    suffices 1 < m → m - (n + 1) % m + min ((n + 1) % m) m = m by
-      simpa [rotateLeft]
-    intro h
-    rw [Nat.min_eq_left (Nat.le_of_lt (Nat.mod_lt _ (by omega)))]
-    have : (n + 1) % m < m := Nat.mod_lt _ (by omega)
-    omega
-
-/-! ### rotateRight -/
-
-@[simp] theorem rotateRight_replicate (n) (a : α) : rotateRight (replicate m a) n = replicate m a := by
-  cases n with
-  | zero => simp
-  | succ n =>
-    suffices 1 < m → m - (m - (n + 1) % m) + min (m - (n + 1) % m) m = m by
-      simpa [rotateRight]
-    intro h
-    have : (n + 1) % m < m := Nat.mod_lt _ (by omega)
-    rw [Nat.min_eq_left (by omega)]
-    omega
-
 /-! ### zipWith -/
 
 @[simp] theorem length_zipWith (f : α → β → γ) (l₁ l₂) :
@@ -336,52 +305,10 @@ theorem take_reverse {α} {xs : List α} (n : Nat) (h : n ≤ xs.length) :
   induction l₁ generalizing l₂ <;> cases l₂ <;>
     simp_all [succ_min_succ, Nat.zero_min, Nat.min_zero]
 
-theorem zipWith_eq_zipWith_take_min : ∀ (l₁ : List α) (l₂ : List β),
-    zipWith f l₁ l₂ = zipWith f (l₁.take (min l₁.length l₂.length)) (l₂.take (min l₁.length l₂.length))
-  | [], _ => by simp
-  | _, [] => by simp
-  | a :: l₁, b :: l₂ => by simp [succ_min_succ, zipWith_eq_zipWith_take_min l₁ l₂]
-
-@[simp] theorem zipWith_replicate {a : α} {b : β} {m n : Nat} :
-    zipWith f (replicate m a) (replicate n b) = replicate (min m n) (f a b) := by
-  rw [zipWith_eq_zipWith_take_min]
-  simp
-
 /-! ### zip -/
 
 @[simp] theorem length_zip (l₁ : List α) (l₂ : List β) :
     length (zip l₁ l₂) = min (length l₁) (length l₂) := by
   simp [zip]
 
-theorem zip_eq_zip_take_min : ∀ (l₁ : List α) (l₂ : List β),
-    zip l₁ l₂ = zip (l₁.take (min l₁.length l₂.length)) (l₂.take (min l₁.length l₂.length))
-  | [], _ => by simp
-  | _, [] => by simp
-  | a :: l₁, b :: l₂ => by simp [succ_min_succ, zip_eq_zip_take_min l₁ l₂]
-
-@[simp] theorem zip_replicate {a : α} {b : β} {m n : Nat} :
-    zip (replicate m a) (replicate n b) = replicate (min m n) (a, b) := by
-  rw [zip_eq_zip_take_min]
-  simp
-
-/-! ### minimum? -/
-
--- A specialization of `minimum?_eq_some_iff` to Nat.
-theorem minimum?_eq_some_iff' {xs : List Nat} :
-    xs.minimum? = some a ↔ (a ∈ xs ∧ ∀ b ∈ xs, a ≤ b) :=
-  minimum?_eq_some_iff
-    (le_refl := Nat.le_refl)
-    (min_eq_or := fun _ _ => by omega)
-    (le_min_iff := fun _ _ _ => by omega)
-
-/-! ### maximum? -/
-
--- A specialization of `maximum?_eq_some_iff` to Nat.
-theorem maximum?_eq_some_iff' {xs : List Nat} :
-    xs.maximum? = some a ↔ (a ∈ xs ∧ ∀ b ∈ xs, b ≤ a) :=
-  maximum?_eq_some_iff
-    (le_refl := Nat.le_refl)
-    (max_eq_or := fun _ _ => by omega)
-    (max_le_iff := fun _ _ _ => by omega)
-
 end List

src/Init/Data/Nat/Basic.lean

@@ -278,7 +278,7 @@ theorem succ_sub_succ_eq_sub (n m : Nat) : succ n - succ m = n - m := by
   | zero      => exact rfl
   | succ m ih => apply congrArg pred ih
 
-theorem pred_le : ∀ (n : Nat), pred n ≤ n
+@[simp] theorem pred_le : ∀ (n : Nat), pred n ≤ n
   | zero   => Nat.le.refl
   | succ _ => le_succ _
 
@@ -288,7 +288,7 @@ theorem pred_lt : ∀ {n : Nat}, n ≠ 0 → pred n < n
 
 theorem sub_one_lt : ∀ {n : Nat}, n ≠ 0 → n - 1 < n := pred_lt
 
-@[simp] theorem sub_le (n m : Nat) : n - m ≤ n := by
+theorem sub_le (n m : Nat) : n - m ≤ n := by
   induction m with
   | zero      => exact Nat.le_refl (n - 0)
   | succ m ih => apply Nat.le_trans (pred_le (n - m)) ih
@@ -636,12 +636,6 @@ theorem succ_le_succ_iff : succ a ≤ succ b ↔ a ≤ b := ⟨le_of_succ_le_suc
 
 theorem succ_lt_succ_iff : succ a < succ b ↔ a < b := ⟨lt_of_succ_lt_succ, succ_lt_succ⟩
 
-theorem add_one_inj : a + 1 = b + 1 ↔ a = b := succ_inj'
-
-theorem add_one_le_add_one_iff : a + 1 ≤ b + 1 ↔ a ≤ b := succ_le_succ_iff
-
-theorem add_one_lt_add_one_iff : a + 1 < b + 1 ↔ a < b := succ_lt_succ_iff
-
 theorem pred_inj : ∀ {a b}, 0 < a → 0 < b → pred a = pred b → a = b
   | _+1, _+1, _, _ => congrArg _
 

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

@@ -310,11 +310,6 @@ theorem testBit_bool_to_nat (b : Bool) (i : Nat) :
         ←Nat.div_div_eq_div_mul _ 2, one_div_two,
         Nat.mod_eq_of_lt]
 
-/-- `testBit 1 i` is true iff the index `i` equals 0. -/
-theorem testBit_one_eq_true_iff_self_eq_zero {i : Nat} :
-    Nat.testBit 1 i = true ↔ i = 0 := by
-  cases i <;> simp
-
 /-! ### bitwise -/
 
 theorem testBit_bitwise

src/Init/Data/Nat/Div.lean

@@ -251,10 +251,10 @@ theorem div_mul_le_self : ∀ (m n : Nat), m / n * n ≤ m
 theorem div_lt_iff_lt_mul (Hk : 0 < k) : x / k < y ↔ x < y * k := by
   rw [← Nat.not_le, ← Nat.not_le]; exact not_congr (le_div_iff_mul_le Hk)
 
-@[simp] theorem add_div_right (x : Nat) {z : Nat} (H : 0 < z) : (x + z) / z = (x / z) + 1 := by
+@[simp] theorem add_div_right (x : Nat) {z : Nat} (H : 0 < z) : (x + z) / z = succ (x / z) := by
   rw [div_eq_sub_div H (Nat.le_add_left _ _), Nat.add_sub_cancel]
 
-@[simp] theorem add_div_left (x : Nat) {z : Nat} (H : 0 < z) : (z + x) / z = (x / z) + 1 := by
+@[simp] theorem add_div_left (x : Nat) {z : Nat} (H : 0 < z) : (z + x) / z = succ (x / z) := by
   rw [Nat.add_comm, add_div_right x H]
 
 theorem add_mul_div_left (x z : Nat) {y : Nat} (H : 0 < y) : (x + y * z) / y = x / y + z := by
@@ -285,7 +285,7 @@ theorem add_mul_div_right (x y : Nat) {z : Nat} (H : 0 < z) : (x + y * z) / z =
 @[simp] theorem mul_mod_left (m n : Nat) : (m * n) % n = 0 := by
   rw [Nat.mul_comm, mul_mod_right]
 
-protected theorem div_eq_of_lt_le (lo : k * n ≤ m) (hi : m < (k + 1) * n) : m / n = k :=
+protected theorem div_eq_of_lt_le (lo : k * n ≤ m) (hi : m < succ k * n) : m / n = k :=
 have npos : 0 < n := (eq_zero_or_pos _).resolve_left fun hn => by
   rw [hn, Nat.mul_zero] at hi lo; exact absurd lo (Nat.not_le_of_gt hi)
 Nat.le_antisymm
@@ -307,7 +307,7 @@ theorem sub_mul_div (x n p : Nat) (h₁ : n*p ≤ x) : (x - n*p) / n = x / n - p
       rw [sub_succ, ← IH h₂, div_eq_sub_div h₀ h₃]
       simp [Nat.pred_succ, mul_succ, Nat.sub_sub]
 
-theorem mul_sub_div (x n p : Nat) (h₁ : x < n*p) : (n * p - (x + 1)) / n = p - ((x / n) + 1) := by
+theorem mul_sub_div (x n p : Nat) (h₁ : x < n*p) : (n * p - succ x) / n = p - succ (x / n) := by
   have npos : 0 < n := (eq_zero_or_pos _).resolve_left fun n0 => by
     rw [n0, Nat.zero_mul] at h₁; exact not_lt_zero _ h₁
   apply Nat.div_eq_of_lt_le

src/Init/Data/Nat/Lemmas.lean

@@ -212,19 +212,13 @@ instance : Std.IdempotentOp (α := Nat) min := ⟨Nat.min_self⟩
 
 @[simp] protected theorem min_zero (a) : min a 0 = 0 := Nat.min_eq_right (Nat.zero_le _)
 
-@[simp] protected theorem min_assoc : ∀ (a b c : Nat), min (min a b) c = min a (min b c)
+protected theorem min_assoc : ∀ (a b c : Nat), min (min a b) c = min a (min b c)
   | 0, _, _ => by rw [Nat.zero_min, Nat.zero_min, Nat.zero_min]
   | _, 0, _ => by rw [Nat.zero_min, Nat.min_zero, Nat.zero_min]
   | _, _, 0 => by rw [Nat.min_zero, Nat.min_zero, Nat.min_zero]
   | _+1, _+1, _+1 => by simp only [Nat.succ_min_succ]; exact congrArg succ <| Nat.min_assoc ..
 instance : Std.Associative (α := Nat) min := ⟨Nat.min_assoc⟩
 
-@[simp] protected theorem min_self_assoc {m n : Nat} : min m (min m n) = min m n := by
-  rw [← Nat.min_assoc, Nat.min_self]
-
-@[simp] protected theorem min_self_assoc' {m n : Nat} : min n (min m n) = min n m := by
-  rw [Nat.min_comm m n, ← Nat.min_assoc, Nat.min_self]
-
 protected theorem sub_sub_eq_min : ∀ (a b : Nat), a - (a - b) = min a b
   | 0, _ => by rw [Nat.zero_sub, Nat.zero_min]
   | _, 0 => by rw [Nat.sub_zero, Nat.sub_self, Nat.min_zero]

src/Init/Data/Nat/Linear.lean

@@ -583,6 +583,8 @@ theorem PolyCnstr.denote_mul (ctx : Context) (k : Nat) (c : PolyCnstr) : (c.mul
   have : k ≠ 0 → k + 1 ≠ 1 := by intro h; match k with | 0 => contradiction | k+1 => simp [Nat.succ.injEq]
   have : ¬ (k == 0) → (k + 1 == 1) = false := fun h => beq_false_of_ne (this (ne_of_beq_false (Bool.of_not_eq_true h)))
   have : ¬ ((k + 1 == 0) = true)  := fun h => absurd (eq_of_beq h) (Nat.succ_ne_zero k)
+  have : (1 == (0 : Nat)) = false := rfl
+  have : (1 == (1 : Nat)) = true  := rfl
   by_cases he : eq = true <;> simp [he, PolyCnstr.mul, PolyCnstr.denote, Poly.denote_le, Poly.denote_eq]
      <;> by_cases hk : k == 0 <;> (try simp [eq_of_beq hk]) <;> simp [*] <;> apply Iff.intro <;> intro h
   · exact Nat.eq_of_mul_eq_mul_left (Nat.zero_lt_succ _) h

src/Init/Data/Option/Basic.lean

@@ -119,7 +119,7 @@ def merge (fn : α → α → α) : Option α → Option α → Option α
 
 
 /-- An elimination principle for `Option`. It is a nondependent version of `Option.recOn`. -/
-@[inline] protected def elim : Option α → β → (α → β) → β
+@[simp, inline] protected def elim : Option α → β → (α → β) → β
   | some x, _, f => f x
   | none, y, _ => y
 

src/Init/Data/Option/Instances.lean

@@ -26,7 +26,7 @@ instance : Membership α (Option α) := ⟨fun a b => b = some a⟩
 instance [DecidableEq α] (j : α) (o : Option α) : Decidable (j ∈ o) :=
   inferInstanceAs <| Decidable (o = some j)
 
-@[simp] theorem isNone_iff_eq_none {o : Option α} : o.isNone ↔ o = none :=
+theorem isNone_iff_eq_none {o : Option α} : o.isNone ↔ o = none :=
   ⟨Option.eq_none_of_isNone, fun e => e.symm ▸ rfl⟩
 
 theorem some_inj {a b : α} : some a = some b ↔ a = b := by simp; rfl

src/Init/Data/Option/Lemmas.lean

@@ -208,9 +208,9 @@ theorem liftOrGet_eq_or_eq {f : α → α → α} (h : ∀ a b, f a b = a ∨ f
 @[simp] theorem liftOrGet_some_some {f} {a b : α} :
   liftOrGet f (some a) (some b) = f a b := rfl
 
-@[simp] theorem elim_none (x : β) (f : α → β) : none.elim x f = x := rfl
+theorem elim_none (x : β) (f : α → β) : none.elim x f = x := rfl
 
-@[simp] theorem elim_some (x : β) (f : α → β) (a : α) : (some a).elim x f = f a := rfl
+theorem elim_some (x : β) (f : α → β) (a : α) : (some a).elim x f = f a := rfl
 
 @[simp] theorem getD_map (f : α → β) (x : α) (o : Option α) :
   (o.map f).getD (f x) = f (getD o x) := by cases o <;> rfl

src/Init/Data/String/Extra.lean

@@ -69,7 +69,7 @@ where
   decreasing_by exact Nat.sub_lt_sub_left ‹_› (Nat.lt_add_of_pos_right c.utf8Size_pos)
 
 /-- Converts a [UTF-8](https://en.wikipedia.org/wiki/UTF-8) encoded `ByteArray` string to `String`. -/
-@[extern "lean_string_from_utf8_unchecked"]
+@[extern "lean_string_from_utf8"]
 def fromUTF8 (a : @& ByteArray) (h : validateUTF8 a) : String :=
   loop 0 ""
 where

src/Init/GetElem.lean

@@ -7,57 +7,22 @@ prelude
 import Init.Util
 
 @[never_extract]
-def outOfBounds [Inhabited α] : α :=
+private def outOfBounds [Inhabited α] : α :=
   panic! "index out of bounds"
 
-theorem outOfBounds_eq_default [Inhabited α] : (outOfBounds : α) = default := rfl
-
 /--
-The classes `GetElem` and `GetElem?` implement lookup notation,
-specifically `xs[i]`, `xs[i]?`, `xs[i]!`, and `xs[i]'p`.
-
-Both classes are indexed by types `coll`, `idx`, and `elem` which are
-the collection, the index, and the element types.
-A single collection may support lookups with multiple index
-types. The relation `valid` determines when the index is guaranteed to be
-valid; lookups of valid indices are guaranteed not to fail.
-
-For example, an instance for arrays looks like
-`GetElem (Array α) Nat α (fun xs i => i < xs.size)`. In other words, given an
-array `xs` and a natural number `i`, `xs[i]` will return an `α` when `valid xs i`
-holds, which is true when `i` is less than the size of the array. `Array`
-additionally supports indexing with `USize` instead of `Nat`.
-In either case, because the bounds are checked at compile time,
-no runtime check is required.
-
+The class `GetElem coll idx elem valid` implements the `xs[i]` notation.
 Given `xs[i]` with `xs : coll` and `i : idx`, Lean looks for an instance of
-`GetElem coll idx elem valid` and uses this to infer the type of the return
-value `elem` and side condition `valid` required to ensure `xs[i]` yields
-a valid value of type `elem`. The tactic `get_elem_tactic` is
-invoked to prove validity automatically. The `xs[i]'p` notation uses the
-proof `p` to satisfy the validity condition.
-If the proof `p` is long, it is often easier to place the
-proof in the context using `have`, because `get_elem_tactic` tries
-`assumption`.
+`GetElem coll idx elem valid` and uses this to infer the type of return
+value `elem` and side conditions `valid` required to ensure `xs[i]` yields
+a valid value of type `elem`.
 
+For example, the instance for arrays looks like
+`GetElem (Array α) Nat α (fun xs i => i < xs.size)`.
 
 The proof side-condition `valid xs i` is automatically dispatched by the
-`get_elem_tactic` tactic; this tactic can be extended by adding more clauses to
-`get_elem_tactic_trivial` using `macro_rules`.
-
-`xs[i]?` and `xs[i]!` do not impose a proof obligation; the former returns
-an `Option elem`, with `none` signalling that the value isn't present, and
-the latter returns `elem` but panics if the value isn't there, returning
-`default : elem` based on the `Inhabited elem` instance.
-These are provided by the `GetElem?` class, for which there is a default instance
-generated from a `GetElem` class as long as `valid xs i` is always decidable.
-
-Important instances include:
-  * `arr[i] : α` where `arr : Array α` and `i : Nat` or `i : USize`: does array
-    indexing with no runtime bounds check and a proof side goal `i < arr.size`.
-  * `l[i] : α` where `l : List α` and `i : Nat`: index into a list, with proof
-    side goal `i < l.length`.
-
+`get_elem_tactic` tactic, which can be extended by adding more clauses to
+`get_elem_tactic_trivial`.
 -/
 class GetElem (coll : Type u) (idx : Type v) (elem : outParam (Type w))
               (valid : outParam (coll → idx → Prop)) where
@@ -65,10 +30,33 @@ class GetElem (coll : Type u) (idx : Type v) (elem : outParam (Type w))
   The syntax `arr[i]` gets the `i`'th element of the collection `arr`. If there
   are proof side conditions to the application, they will be automatically
   inferred by the `get_elem_tactic` tactic.
+
+  The actual behavior of this class is type-dependent, but here are some
+  important implementations:
+  * `arr[i] : α` where `arr : Array α` and `i : Nat` or `i : USize`: does array
+    indexing with no bounds check and a proof side goal `i < arr.size`.
+  * `l[i] : α` where `l : List α` and `i : Nat`: index into a list, with proof
+    side goal `i < l.length`.
+  * `stx[i] : Syntax` where `stx : Syntax` and `i : Nat`: get a syntax argument,
+    no side goal (returns `.missing` out of range)
+
+  There are other variations on this syntax:
+  * `arr[i]!` is syntax for `getElem! arr i` which should panic and return
+    `default : α` if the index is not valid.
+  * `arr[i]?` is syntax for `getElem?` which should return `none` if the index
+    is not valid.
+  * `arr[i]'h` is syntax for `getElem arr i h` with `h` an explicit proof the
+    index is valid.
   -/
   getElem (xs : coll) (i : idx) (h : valid xs i) : elem
 
-export GetElem (getElem)
+  getElem? (xs : coll) (i : idx) [Decidable (valid xs i)] : Option elem :=
+    if h : _ then some (getElem xs i h) else none
+
+  getElem! [Inhabited elem] (xs : coll) (i : idx) [Decidable (valid xs i)] : elem :=
+    match getElem? xs i with | some e => e | none => outOfBounds
+
+export GetElem (getElem getElem! getElem?)
 
 @[inherit_doc getElem]
 syntax:max term noWs "[" withoutPosition(term) "]" : term
@@ -78,30 +66,6 @@ macro_rules | `($x[$i]) => `(getElem $x $i (by get_elem_tactic))
 syntax term noWs "[" withoutPosition(term) "]'" term:max : term
 macro_rules | `($x[$i]'$h) => `(getElem $x $i $h)
 
-/-- Helper function for implementation of `GetElem?.getElem?`. -/
-abbrev decidableGetElem? [GetElem coll idx elem valid] (xs : coll) (i : idx) [Decidable (valid xs i)] :
-    Option elem :=
-  if h : valid xs i then some xs[i] else none
-
-@[inherit_doc GetElem]
-class GetElem? (coll : Type u) (idx : Type v) (elem : outParam (Type w))
-    (valid : outParam (coll → idx → Prop)) extends GetElem coll idx elem valid where
-  /--
-  The syntax `arr[i]?` gets the `i`'th element of the collection `arr`,
-  if it is present (and wraps it in `some`), and otherwise returns `none`.
-  -/
-  getElem? : coll → idx → Option elem
-
-  /--
-  The syntax `arr[i]!` gets the `i`'th element of the collection `arr`,
-  if it is present, and otherwise panics at runtime and returns the `default` term
-  from `Inhabited elem`.
-  -/
-  getElem! [Inhabited elem] (xs : coll) (i : idx) : elem :=
-    match getElem? xs i with | some e => e | none => outOfBounds
-
-export GetElem? (getElem? getElem!)
-
 /--
 The syntax `arr[i]?` gets the `i`'th element of the collection `arr` or
 returns `none` if `i` is out of bounds.
@@ -114,43 +78,32 @@ panics `i` is out of bounds.
 -/
 macro:max x:term noWs "[" i:term "]" noWs "!" : term => `(getElem! $x $i)
 
-instance (priority := low) [GetElem coll idx elem valid] [∀ xs i, Decidable (valid xs i)] :
-    GetElem? coll idx elem valid where
-  getElem? xs i := decidableGetElem? xs i
-
 class LawfulGetElem (cont : Type u) (idx : Type v) (elem : outParam (Type w))
-   (dom : outParam (cont → idx → Prop)) [ge : GetElem? cont idx elem dom] : Prop where
+   (dom : outParam (cont → idx → Prop)) [ge : GetElem cont idx elem dom] : Prop where
 
   getElem?_def (c : cont) (i : idx) [Decidable (dom c i)] :
-      c[i]? = if h : dom c i then some (c[i]'h) else none := by
-    intros
-    try simp only [getElem?] <;> congr
-  getElem!_def [Inhabited elem] (c : cont) (i : idx) :
-      c[i]! = match c[i]? with | some e => e | none => default := by
-    intros
-    simp only [getElem!, getElem?, outOfBounds_eq_default]
+    c[i]? = if h : dom c i then some (c[i]'h) else none := by intros; eq_refl
+  getElem!_def [Inhabited elem] (c : cont) (i : idx) [Decidable (dom c i)] :
+    c[i]! = match c[i]? with | some e => e | none => default := by intros; eq_refl
 
 export LawfulGetElem (getElem?_def getElem!_def)
 
-instance (priority := low) [GetElem coll idx elem valid] [∀ xs i, Decidable (valid xs i)] :
-    LawfulGetElem coll idx elem valid where
-
-theorem getElem?_pos [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
+theorem getElem?_pos [GetElem cont idx elem dom] [LawfulGetElem cont idx elem dom]
     (c : cont) (i : idx) (h : dom c i) [Decidable (dom c i)] : c[i]? = some (c[i]'h) := by
   rw [getElem?_def]
   exact dif_pos h
 
-theorem getElem?_neg [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
+theorem getElem?_neg [GetElem cont idx elem dom] [LawfulGetElem cont idx elem dom]
     (c : cont) (i : idx) (h : ¬dom c i) [Decidable (dom c i)] : c[i]? = none := by
   rw [getElem?_def]
   exact dif_neg h
 
-theorem getElem!_pos [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
+theorem getElem!_pos [GetElem cont idx elem dom] [LawfulGetElem cont idx elem dom]
     [Inhabited elem] (c : cont) (i : idx) (h : dom c i) [Decidable (dom c i)] :
     c[i]! = c[i]'h := by
   simp only [getElem!_def, getElem?_def, h]
 
-theorem getElem!_neg [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
+theorem getElem!_neg [GetElem cont idx elem dom] [LawfulGetElem cont idx elem dom]
     [Inhabited elem] (c : cont) (i : idx) (h : ¬dom c i) [Decidable (dom c i)] : c[i]! = default := by
   simp only [getElem!_def, getElem?_def, h]
 
@@ -158,23 +111,22 @@ namespace Fin
 
 instance instGetElemFinVal [GetElem cont Nat elem dom] : GetElem cont (Fin n) elem fun xs i => dom xs i where
   getElem xs i h := getElem xs i.1 h
-
-instance instGetElem?FinVal [GetElem? cont Nat elem dom] : GetElem? cont (Fin n) elem fun xs i => dom xs i where
   getElem? xs i := getElem? xs i.val
   getElem! xs i := getElem! xs i.val
 
-instance [GetElem? cont Nat elem dom] [h : LawfulGetElem cont Nat elem dom] :
+instance [GetElem cont Nat elem dom] [h : LawfulGetElem cont Nat elem dom] :
       LawfulGetElem cont (Fin n) elem fun xs i => dom xs i where
-  getElem?_def _c _i _d := h.getElem?_def ..
-  getElem!_def _c _i := h.getElem!_def ..
 
-@[simp] theorem getElem_fin [GetElem? Cont Nat Elem Dom] (a : Cont) (i : Fin n) (h : Dom a i) :
+  getElem?_def _c _i _d := h.getElem?_def ..
+  getElem!_def _c _i _d := h.getElem!_def ..
+
+@[simp] theorem getElem_fin [GetElem Cont Nat Elem Dom] (a : Cont) (i : Fin n) (h : Dom a i) :
     a[i] = a[i.1] := rfl
 
-@[simp] theorem getElem?_fin [h : GetElem? Cont Nat Elem Dom] (a : Cont) (i : Fin n)
+@[simp] theorem getElem?_fin [h : GetElem Cont Nat Elem Dom] (a : Cont) (i : Fin n)
     [Decidable (Dom a i)] : a[i]? = a[i.1]? := by rfl
 
-@[simp] theorem getElem!_fin [GetElem? Cont Nat Elem Dom] (a : Cont) (i : Fin n)
+@[simp] theorem getElem!_fin [GetElem Cont Nat Elem Dom] (a : Cont) (i : Fin n)
     [Decidable (Dom a i)] [Inhabited Elem] : a[i]! = a[i.1]! := rfl
 
 macro_rules
@@ -187,6 +139,8 @@ namespace List
 instance : GetElem (List α) Nat α fun as i => i < as.length where
   getElem as i h := as.get ⟨i, h⟩
 
+instance : LawfulGetElem (List α) Nat α fun as i => i < as.length where
+
 @[simp] theorem getElem_cons_zero (a : α) (as : List α) (h : 0 < (a :: as).length) : getElem (a :: as) 0 h = a := by
   rfl
 
@@ -209,6 +163,8 @@ namespace Array
 instance : GetElem (Array α) Nat α fun xs i => i < xs.size where
   getElem xs i h := xs.get ⟨i, h⟩
 
+instance : LawfulGetElem (Array α) Nat α fun xs i => i < xs.size where
+
 end Array
 
 namespace Lean.Syntax
@@ -216,4 +172,6 @@ namespace Lean.Syntax
 instance : GetElem Syntax Nat Syntax fun _ _ => True where
   getElem stx i _ := stx.getArg i
 
+instance : LawfulGetElem Syntax Nat Syntax fun _ _ => True where
+
 end Lean.Syntax

src/Init/Meta.lean

@@ -1278,46 +1278,12 @@ def Occurrences.isAll : Occurrences → Bool
   | all => true
   | _   => false
 
-/--
-Controls which new mvars are turned in to goals by the `apply` tactic.
-- `nonDependentFirst`  mvars that don't depend on other goals appear first in the goal list.
-- `nonDependentOnly` only mvars that don't depend on other goals are added to goal list.
-- `all` all unassigned mvars are added to the goal list.
--/
--- TODO: Consider renaming to `Apply.NewGoals`
-inductive ApplyNewGoals where
-  | nonDependentFirst | nonDependentOnly | all
-
-/-- Configures the behaviour of the `apply` tactic. -/
--- TODO: Consider renaming to `Apply.Config`
-structure ApplyConfig where
-  newGoals := ApplyNewGoals.nonDependentFirst
-  /--
-  If `synthAssignedInstances` is `true`, then `apply` will synthesize instance implicit arguments
-  even if they have assigned by `isDefEq`, and then check whether the synthesized value matches the
-  one inferred. The `congr` tactic sets this flag to false.
-  -/
-  synthAssignedInstances := true
-  /--
-  If `allowSynthFailures` is `true`, then `apply` will return instance implicit arguments
-  for which typeclass search failed as new goals.
-  -/
-  allowSynthFailures := false
-  /--
-  If `approx := true`, then we turn on `isDefEq` approximations. That is, we use
-  the `approxDefEq` combinator.
-  -/
-  approx : Bool := true
-
 namespace Rewrite
 
-abbrev NewGoals := ApplyNewGoals
-
 structure Config where
-  transparency : TransparencyMode := .reducible
+  transparency : TransparencyMode := TransparencyMode.reducible
   offsetCnstrs : Bool := true
-  occs : Occurrences := .all
-  newGoals : NewGoals := .nonDependentFirst
+  occs : Occurrences := Occurrences.all
 
 end Rewrite
 

src/Init/MetaTypes.lean

@@ -42,67 +42,23 @@ inductive EtaStructMode where
 
 namespace DSimp
 
-/--
-The configuration for `dsimp`.
-Passed to `dsimp` using, for example, the `dsimp (config := {zeta := false})` syntax.
-
-Implementation note: this structure is only used for processing the `(config := ...)` syntax, and it is not used internally.
-It is immediately converted to `Lean.Meta.Simp.Config` by `Lean.Elab.Tactic.elabSimpConfig`.
--/
 structure Config where
-  /--
-  When `true` (default: `true`), performs zeta reduction of let expressions.
-  That is, `let x := v; e[x]` reduces to `e[v]`.
-  See also `zetaDelta`.
-  -/
+  /-- `let x := v; e[x]` reduces to `e[v]`. -/
   zeta              : Bool := true
-  /--
-  When `true` (default: `true`), performs beta reduction of applications of `fun` expressions.
-  That is, `(fun x => e[x]) v` reduces to `e[v]`.
-  -/
   beta              : Bool := true
-  /--
-  TODO (currently unimplemented). When `true` (default: `true`), performs eta reduction for `fun` expressions.
-  That is, `(fun x => f x)` reduces to `f`.
-  -/
   eta               : Bool := true
-  /--
-  Configures how to determine definitional equality between two structure instances.
-  See documentation for `Lean.Meta.EtaStructMode`.
-  -/
   etaStruct         : EtaStructMode := .all
-  /--
-  When `true` (default: `true`), reduces `match` expressions applied to constructors.
-  -/
   iota              : Bool := true
-  /--
-  When `true` (default: `true`), reduces projections of structure constructors.
-  -/
   proj              : Bool := true
-  /--
-  When `true` (default: `false`), rewrites a proposition `p` to `True` or `False` by inferring
-  a `Decidable p` instance and reducing it.
-  -/
   decide            : Bool := false
-  /--
-  When `true` (default: `false`), unfolds definitions.
-  This can be enabled using the `simp!` syntax.
-  -/
   autoUnfold        : Bool := false
-  /--
-  If `failIfUnchanged` is `true` (default: `true`), then calls to `simp`, `dsimp`, or `simp_all`
-  will fail if they do not make progress.
-  -/
+  /-- If `failIfUnchanged := true`, then calls to `simp`, `dsimp`, or `simp_all`
+  will fail if they do not make progress. -/
   failIfUnchanged   : Bool := true
-  /--
-  If `unfoldPartialApp` is `true` (default: `false`), then calls to `simp`, `dsimp`, or `simp_all`
-  will unfold even partial applications of `f` when we request `f` to be unfolded.
-  -/
+  /-- If `unfoldPartialApp := true`, then calls to `simp`, `dsimp`, or `simp_all`
+  will unfold even partial applications of `f` when we request `f` to be unfolded. -/
   unfoldPartialApp  : Bool := false
-  /--
-  When `true` (default: `false`), local definitions are unfolded.
-  That is, given a local context containing entry `x : t := e`, the free variable `x` reduces to `e`.
-  -/
+  /-- Given a local context containing entry `x : t := e`, free variable `x` reduces to `e`. -/
   zetaDelta         : Bool := false
   deriving Inhabited, BEq
 
@@ -116,7 +72,7 @@ def defaultMaxSteps := 100000
 The configuration for `simp`.
 Passed to `simp` using, for example, the `simp (config := {contextual := true})` syntax.
 
-See also `Lean.Meta.Simp.neutralConfig` and `Lean.Meta.DSimp.Config`.
+See also `Lean.Meta.Simp.neutralConfig`.
 -/
 structure Config where
   /--

src/Init/Notation.lean

@@ -558,22 +558,6 @@ syntax (name := runMeta) "run_meta " doSeq : command
 set_option linter.missingDocs false in
 syntax guardMsgsFilterSeverity := &"info" <|> &"warning" <|> &"error" <|> &"all"
 
-/--
-`#reduce <expression>` reduces the expression `<expression>` to its normal form. This
-involves applying reduction rules until no further reduction is possible.
-
-By default, proofs and types within the expression are not reduced. Use modifiers
-`(proofs := true)`  and `(types := true)` to reduce them.
-Recall that propositions are types in Lean.
-
-**Warning:** This can be a computationally expensive operation,
-especially for complex expressions.
-
-Consider using `#eval <expression>` for simple evaluation/execution
-of expressions.
--/
-syntax (name := reduceCmd) "#reduce " (atomic("(" &"proofs" " := " &"true" ")"))? (atomic("(" &"types" " := " &"true" ")"))? term : command
-
 /--
 A message filter specification for `#guard_msgs`.
 - `info`, `warning`, `error`: capture messages with the given severity level.

src/Init/Omega/IntList.lean

@@ -173,7 +173,7 @@ theorem mul_neg_left (xs ys : IntList) : (-xs) * ys = -(xs * ys) := by
 attribute [local simp] add_def neg_def sub_def in
 theorem sub_eq_add_neg (xs ys : IntList) : xs - ys = xs + (-ys) := by
   induction xs generalizing ys with
-  | nil => simp
+  | nil => simp; rfl
   | cons x xs ih =>
     cases ys with
     | nil => simp

src/Init/Prelude.lean

@@ -740,7 +740,7 @@ prove `p` given any element `x : α`, then `p` holds. Note that it is essential
 that `p` is a `Prop` here; the version with `p` being a `Sort u` is equivalent
 to `Classical.choice`.
 -/
-protected theorem Nonempty.elim {α : Sort u} {p : Prop} (h₁ : Nonempty α) (h₂ : α → p) : p :=
+protected def Nonempty.elim {α : Sort u} {p : Prop} (h₁ : Nonempty α) (h₂ : α → p) : p :=
   match h₁ with
   | intro a => h₂ a
 
@@ -2329,6 +2329,9 @@ without running out of stack space.
 def List.lengthTR (as : List α) : Nat :=
   lengthTRAux as 0
 
+@[simp] theorem List.length_cons {α} (a : α) (as : List α) : Eq (cons a as).length as.length.succ :=
+  rfl
+
 /--
 `as.get i` returns the `i`'th element of the list `as`.
 This version of the function uses `i : Fin as.length` to ensure that it will
@@ -2973,7 +2976,7 @@ def MonadExcept.ofExcept [Monad m] [MonadExcept ε m] : Except ε α → m α
 
 export MonadExcept (throw tryCatch ofExcept)
 
-instance (ε : Type u) (m : Type v → Type w) [MonadExceptOf ε m] : MonadExcept ε m where
+instance (ε : outParam (Type u)) (m : Type v → Type w) [MonadExceptOf ε m] : MonadExcept ε m where
   throw    := throwThe ε
   tryCatch := tryCatchThe ε
 
@@ -3147,7 +3150,7 @@ instance (ρ : Type u) (m : Type u → Type v) [MonadWithReaderOf ρ m] : MonadW
 instance {ρ : Type u} {m : Type u → Type v} {n : Type u → Type v} [MonadFunctor m n] [MonadWithReaderOf ρ m] : MonadWithReaderOf ρ n where
   withReader f := monadMap (m := m) (withTheReader ρ f)
 
-instance {ρ : Type u} {m : Type u → Type v} : MonadWithReaderOf ρ (ReaderT ρ m) where
+instance {ρ : Type u} {m : Type u → Type v} [Monad m] : MonadWithReaderOf ρ (ReaderT ρ m) where
   withReader f x := fun ctx => x (f ctx)
 
 /--
@@ -3230,7 +3233,7 @@ def modify {σ : Type u} {m : Type u → Type v} [MonadState σ m] (f : σ →
 of the state. It is equivalent to `get <* modify f` but may be more efficient.
 -/
 @[always_inline, inline]
-def getModify {σ : Type u} {m : Type u → Type v} [MonadState σ m] (f : σ → σ) : m σ :=
+def getModify {σ : Type u} {m : Type u → Type v} [MonadState σ m] [Monad m] (f : σ → σ) : m σ :=
   modifyGet fun s => (s, f s)
 
 -- NOTE: The Ordering of the following two instances determines that the top-most `StateT` Monad layer

src/Init/Tactics.lean

@@ -267,9 +267,7 @@ syntax (name := case') "case' " sepBy1(caseArg, " | ") " => " tacticSeq : tactic
 `next x₁ ... xₙ => tac` additionally renames the `n` most recent hypotheses with
 inaccessible names to the given names.
 -/
-macro "next " args:binderIdent* arrowTk:" => " tac:tacticSeq : tactic =>
-  -- Limit ref variability for incrementality; see Note [Incremental Macros]
-  withRef arrowTk `(tactic| case _ $args* =>%$arrowTk $tac)
+macro "next " args:binderIdent* " => " tac:tacticSeq : tactic => `(tactic| case _ $args* => $tac)
 
 /-- `all_goals tac` runs `tac` on each goal, concatenating the resulting goals, if any. -/
 syntax (name := allGoals) "all_goals " tacticSeq : tactic
@@ -373,8 +371,7 @@ reflexivity theorems (e.g., `Iff.rfl`).
 macro "rfl" : tactic => `(tactic| case' _ => fail "The rfl tactic failed. Possible reasons:
 - The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma).
 - The arguments of the relation are not equal.
-Try using the reflexivity lemma for your relation explicitly, e.g. `exact Eq.refl _` or
-`exact HEq.rfl` etc.")
+Try using the reflexivitiy lemma for your relation explicitly, e.g. `exact Eq.rfl`.")
 
 macro_rules | `(tactic| rfl) => `(tactic| eq_refl)
 macro_rules | `(tactic| rfl) => `(tactic| exact HEq.rfl)
@@ -1462,7 +1459,6 @@ have been simplified by using the modifier `↓`. Here is an example
 ```
 
 When multiple simp theorems are applicable, the simplifier uses the one with highest priority.
-The equational theorems of function are applied at very low priority (100 and below).
 If there are several with the same priority, it is uses the "most recent one". Example:
 ```lean
 @[simp high] theorem cond_true (a b : α) : cond true a b = a := rfl

src/Init/TacticsExtra.lean

@@ -31,19 +31,15 @@ private def expandIfThenElse
       pure (hole, #[case])
   let (posHole, posCase) ← mkCase thenTk pos `(?pos)
   let (negHole, negCase) ← mkCase elseTk neg `(?neg)
-  `(tactic| ((open Classical in refine%$ifTk $(← mkIf posHole negHole)); $[$(posCase ++ negCase)]*))
+  `(tactic| (open Classical in refine%$ifTk $(← mkIf posHole negHole); $[$(posCase ++ negCase)]*))
 
 macro_rules
   | `(tactic| if%$tk $h : $c then%$ttk $pos else%$etk $neg) =>
-    -- Limit ref variability for incrementality; see Note [Incremental Macros]
-    withRef tk do
-      expandIfThenElse tk ttk etk pos neg fun pos neg => `(if $h : $c then $pos else $neg)
+    expandIfThenElse tk ttk etk pos neg fun pos neg => `(if $h : $c then $pos else $neg)
 
 macro_rules
   | `(tactic| if%$tk $c then%$ttk $pos else%$etk $neg) =>
-    -- Limit ref variability for incrementality; see Note [Incremental Macros]
-    withRef tk do
-      expandIfThenElse tk ttk etk pos neg fun pos neg => `(if h : $c then $pos else $neg)
+    expandIfThenElse tk ttk etk pos neg fun pos neg => `(if h : $c then $pos else $neg)
 
 /--
 `iterate n tac` runs `tac` exactly `n` times.

src/Init/WF.lean

@@ -37,7 +37,7 @@ noncomputable abbrev Acc.ndrecOn.{u1, u2} {α : Sort u2} {r : α → α → Prop
 namespace Acc
 variable {α : Sort u} {r : α → α → Prop}
 
-theorem inv {x y : α} (h₁ : Acc r x) (h₂ : r y x) : Acc r y :=
+def inv {x y : α} (h₁ : Acc r x) (h₂ : r y x) : Acc r y :=
   h₁.recOn (fun _ ac₁ _ h₂ => ac₁ y h₂) h₂
 
 end Acc
@@ -58,7 +58,7 @@ class WellFoundedRelation (α : Sort u) where
   wf  : WellFounded rel
 
 namespace WellFounded
-theorem apply {α : Sort u} {r : α → α → Prop} (wf : WellFounded r) (a : α) : Acc r a :=
+def apply {α : Sort u} {r : α → α → Prop} (wf : WellFounded r) (a : α) : Acc r a :=
   wf.rec (fun p => p) a
 
 section
@@ -78,7 +78,7 @@ noncomputable def fixF (x : α) (a : Acc r x) : C x := by
   induction a with
   | intro x₁ _ ih => exact F x₁ ih
 
-theorem fixFEq (x : α) (acx : Acc r x) : fixF F x acx = F x (fun (y : α) (p : r y x) => fixF F y (Acc.inv acx p)) := by
+def fixFEq (x : α) (acx : Acc r x) : fixF F x acx = F x (fun (y : α) (p : r y x) => fixF F y (Acc.inv acx p)) := by
   induction acx with
   | intro x r _ => exact rfl
 
@@ -112,14 +112,14 @@ def emptyWf {α : Sort u} : WellFoundedRelation α where
 namespace Subrelation
 variable {α : Sort u} {r q : α → α → Prop}
 
-theorem accessible {a : α} (h₁ : Subrelation q r) (ac : Acc r a) : Acc q a := by
+def accessible {a : α} (h₁ : Subrelation q r) (ac : Acc r a) : Acc q a := by
   induction ac with
   | intro x _ ih =>
     apply Acc.intro
     intro y h
     exact ih y (h₁ h)
 
-theorem wf (h₁ : Subrelation q r) (h₂ : WellFounded r) : WellFounded q :=
+def wf (h₁ : Subrelation q r) (h₂ : WellFounded r) : WellFounded q :=
   ⟨fun a => accessible @h₁ (apply h₂ a)⟩
 end Subrelation
 
@@ -136,10 +136,10 @@ private def accAux (f : α → β) {b : β} (ac : Acc r b) : (x : α) → f x =
     subst x
     apply ih (f y) lt y rfl
 
-theorem accessible {a : α} (f : α → β) (ac : Acc r (f a)) : Acc (InvImage r f) a :=
+def accessible {a : α} (f : α → β) (ac : Acc r (f a)) : Acc (InvImage r f) a :=
   accAux f ac a rfl
 
-theorem wf (f : α → β) (h : WellFounded r) : WellFounded (InvImage r f) :=
+def wf (f : α → β) (h : WellFounded r) : WellFounded (InvImage r f) :=
   ⟨fun a => accessible f (apply h (f a))⟩
 end InvImage
 
@@ -151,7 +151,7 @@ end InvImage
 namespace TC
 variable {α : Sort u} {r : α → α → Prop}
 
-theorem accessible {z : α} (ac : Acc r z) : Acc (TC r) z := by
+def accessible {z : α} (ac : Acc r z) : Acc (TC r) z := by
   induction ac with
   | intro x acx ih =>
     apply Acc.intro x
@@ -160,7 +160,7 @@ theorem accessible {z : α} (ac : Acc r z) : Acc (TC r) z := by
     | base a b rab => exact ih a rab
     | trans a b c rab _ _ ih₂ => apply Acc.inv (ih₂ acx ih) rab
 
-theorem wf (h : WellFounded r) : WellFounded (TC r) :=
+def wf (h : WellFounded r) : WellFounded (TC r) :=
   ⟨fun a => accessible (apply h a)⟩
 end TC
 
@@ -251,7 +251,7 @@ instance [αeqDec : DecidableEq α] {r : α → α → Prop} [rDec : DecidableRe
         apply isFalse; intro contra; cases contra <;> contradiction
 
 -- TODO: generalize
-theorem right' {a₁ : Nat} {b₁ : β} (h₁ : a₁ ≤ a₂) (h₂ : rb b₁ b₂) : Prod.Lex Nat.lt rb (a₁, b₁) (a₂, b₂) :=
+def right' {a₁ : Nat} {b₁ : β} (h₁ : a₁ ≤ a₂) (h₂ : rb b₁ b₂) : Prod.Lex Nat.lt rb (a₁, b₁) (a₂, b₂) :=
   match Nat.eq_or_lt_of_le h₁ with
   | Or.inl h => h ▸ Prod.Lex.right a₁ h₂
   | Or.inr h => Prod.Lex.left b₁ _ h
@@ -268,7 +268,7 @@ section
 variable {α : Type u} {β : Type v}
 variable {ra  : α → α → Prop} {rb  : β → β → Prop}
 
-theorem lexAccessible {a : α} (aca : Acc ra a) (acb : (b : β) → Acc rb b) (b : β) : Acc (Prod.Lex ra rb) (a, b) := by
+def lexAccessible {a : α} (aca : Acc ra a) (acb : (b : β) → Acc rb b) (b : β) : Acc (Prod.Lex ra rb) (a, b) := by
   induction aca generalizing b with
   | intro xa _ iha =>
     induction (acb b) with
@@ -347,7 +347,7 @@ variable {α : Sort u} {β : Sort v}
 def lexNdep (r : α → α → Prop) (s : β → β → Prop) :=
   Lex r (fun _ => s)
 
-theorem lexNdepWf {r  : α → α → Prop} {s : β → β → Prop} (ha : WellFounded r) (hb : WellFounded s) : WellFounded (lexNdep r s) :=
+def lexNdepWf {r  : α → α → Prop} {s : β → β → Prop} (ha : WellFounded r) (hb : WellFounded s) : WellFounded (lexNdep r s) :=
   WellFounded.intro fun ⟨a, b⟩ => lexAccessible (WellFounded.apply ha a) (fun _ => hb) b
 end
 
@@ -365,7 +365,7 @@ open WellFounded
 variable {α : Sort u} {β : Sort v}
 variable {r  : α → α → Prop} {s : β → β → Prop}
 
-theorem revLexAccessible {b} (acb : Acc s b) (aca : (a : α) → Acc r a): (a : α) → Acc (RevLex r s) ⟨a, b⟩ := by
+def revLexAccessible {b} (acb : Acc s b) (aca : (a : α) → Acc r a): (a : α) → Acc (RevLex r s) ⟨a, b⟩ := by
   induction acb with
   | intro xb _ ihb =>
     intro a
@@ -377,7 +377,7 @@ theorem revLexAccessible {b} (acb : Acc s b) (aca : (a : α) → Acc r a): (a :
       | left  => apply iha; assumption
       | right => apply ihb; assumption
 
-theorem revLex (ha : WellFounded r) (hb : WellFounded s) : WellFounded (RevLex r s) :=
+def revLex (ha : WellFounded r) (hb : WellFounded s) : WellFounded (RevLex r s) :=
   WellFounded.intro fun ⟨a, b⟩ => revLexAccessible (apply hb b) (WellFounded.apply ha) a
 end
 
@@ -389,7 +389,7 @@ def skipLeft (α : Type u) {β : Type v} (hb : WellFoundedRelation β) : WellFou
   rel := SkipLeft α hb.rel
   wf  := revLex emptyWf.wf hb.wf
 
-theorem mkSkipLeft {α : Type u} {β : Type v} {b₁ b₂ : β} {s : β → β → Prop} (a₁ a₂ : α) (h : s b₁ b₂) : SkipLeft α s ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ :=
+def mkSkipLeft {α : Type u} {β : Type v} {b₁ b₂ : β} {s : β → β → Prop} (a₁ a₂ : α) (h : s b₁ b₂) : SkipLeft α s ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ :=
   RevLex.right _ _ h
 end
 

src/Lean/AddDecl.lean

@@ -8,17 +8,8 @@ import Lean.CoreM
 
 namespace Lean
 
-register_builtin_option debug.skipKernelTC : Bool := {
-  defValue := false
-  group    := "debug"
-  descr    := "skip kernel type checker. WARNING: setting this option to true may compromise soundness because your proofs will not be checked by the Lean kernel"
-}
-
 def Environment.addDecl (env : Environment) (opts : Options) (decl : Declaration) : Except KernelException Environment :=
-  if debug.skipKernelTC.get opts then
-    addDeclWithoutChecking env decl
-  else
-    addDeclCore env (Core.getMaxHeartbeats opts).toUSize decl
+  addDeclCore env (Core.getMaxHeartbeats opts).toUSize decl
 
 def Environment.addAndCompile (env : Environment) (opts : Options) (decl : Declaration) : Except KernelException Environment := do
   let env ← addDecl env opts decl

src/Lean/Attributes.lean

@@ -53,7 +53,7 @@ structure AttributeImpl extends AttributeImplCore where
   erase (decl : Name) : AttrM Unit := throwError "attribute cannot be erased"
   deriving Inhabited
 
-builtin_initialize attributeMapRef : IO.Ref (HashMap Name AttributeImpl) ← IO.mkRef {}
+builtin_initialize attributeMapRef : IO.Ref (PersistentHashMap Name AttributeImpl) ← IO.mkRef {}
 
 /-- Low level attribute registration function. -/
 def registerBuiltinAttribute (attr : AttributeImpl) : IO Unit := do
@@ -185,7 +185,7 @@ structure ParametricAttributeImpl (α : Type) extends AttributeImplCore where
   afterSet : Name → α → AttrM Unit := fun _ _ _ => pure ()
   afterImport : Array (Array (Name × α)) → ImportM Unit := fun _ => pure ()
 
-def registerParametricAttribute (impl : ParametricAttributeImpl α) : IO (ParametricAttribute α) := do
+def registerParametricAttribute [Inhabited α] (impl : ParametricAttributeImpl α) : IO (ParametricAttribute α) := do
   let ext : PersistentEnvExtension (Name × α) (Name × α) (NameMap α) ← registerPersistentEnvExtension {
     name            := impl.ref
     mkInitial       := pure {}
@@ -239,7 +239,7 @@ structure EnumAttributes (α : Type) where
   ext   : PersistentEnvExtension (Name × α) (Name × α) (NameMap α)
   deriving Inhabited
 
-def registerEnumAttributes (attrDescrs : List (Name × String × α))
+def registerEnumAttributes [Inhabited α] (attrDescrs : List (Name × String × α))
     (validate : Name → α → AttrM Unit := fun _ _ => pure ())
     (applicationTime := AttributeApplicationTime.afterTypeChecking)
     (ref : Name := by exact decl_name%) : IO (EnumAttributes α) := do
@@ -317,7 +317,7 @@ inductive AttributeExtensionOLeanEntry where
 
 structure AttributeExtensionState where
   newEntries : List AttributeExtensionOLeanEntry := []
-  map        : HashMap Name AttributeImpl
+  map        : PersistentHashMap Name AttributeImpl
   deriving Inhabited
 
 abbrev AttributeExtension := PersistentEnvExtension AttributeExtensionOLeanEntry (AttributeExtensionOLeanEntry × AttributeImpl) AttributeExtensionState
@@ -348,7 +348,7 @@ private def AttributeExtension.addImported (es : Array (Array AttributeExtension
   let map ← es.foldlM
     (fun map entries =>
       entries.foldlM
-        (fun (map : HashMap Name AttributeImpl) entry => do
+        (fun (map : PersistentHashMap Name AttributeImpl) entry => do
           let attrImpl ← mkAttributeImplOfEntry ctx.env ctx.opts entry
           return map.insert attrImpl.name attrImpl)
         map)
@@ -374,7 +374,7 @@ def isBuiltinAttribute (n : Name) : IO Bool := do
 
 /-- Return the name of all registered attributes. -/
 def getBuiltinAttributeNames : IO (List Name) :=
-  return (← attributeMapRef.get).fold (init := []) fun r n _ => n::r
+  return (← attributeMapRef.get).foldl (init := []) fun r n _ => n::r
 
 def getBuiltinAttributeImpl (attrName : Name) : IO AttributeImpl := do
   let m ← attributeMapRef.get
@@ -392,7 +392,7 @@ def isAttribute (env : Environment) (attrName : Name) : Bool :=
 
 def getAttributeNames (env : Environment) : List Name :=
   let m := (attributeExtension.getState env).map
-  m.fold (fun r n _ => n::r) []
+  m.foldl (fun r n _ => n::r) []
 
 def getAttributeImpl (env : Environment) (attrName : Name) : Except String AttributeImpl :=
   let m := (attributeExtension.getState env).map
@@ -427,7 +427,7 @@ def Attribute.erase (declName : Name) (attrName : Name) : AttrM Unit := do
 def updateEnvAttributesImpl (env : Environment) : IO Environment := do
   let map ← attributeMapRef.get
   let s := attributeExtension.getState env
-  let s := map.fold (init := s) fun s attrName attrImpl =>
+  let s := map.foldl (init := s) fun s attrName attrImpl =>
     if s.map.contains attrName then
       s
     else

src/Lean/AuxRecursor.lean

@@ -13,17 +13,16 @@ def recOnSuffix         := "recOn"
 def brecOnSuffix        := "brecOn"
 def binductionOnSuffix  := "binductionOn"
 def belowSuffix         := "below"
-def ibelowSuffix        := "ibelow"
 
 def mkCasesOnName (indDeclName : Name) : Name := Name.mkStr indDeclName casesOnSuffix
 def mkRecOnName (indDeclName : Name) : Name   := Name.mkStr indDeclName recOnSuffix
 def mkBRecOnName (indDeclName : Name) : Name  := Name.mkStr indDeclName brecOnSuffix
 def mkBInductionOnName (indDeclName : Name) : Name  := Name.mkStr indDeclName binductionOnSuffix
 def mkBelowName (indDeclName : Name) : Name := Name.mkStr indDeclName belowSuffix
-def mkIBelowName (indDeclName : Name) : Name := Name.mkStr indDeclName ibelowSuffix
 
 builtin_initialize auxRecExt : TagDeclarationExtension ← mkTagDeclarationExtension
 
+@[export lean_mark_aux_recursor]
 def markAuxRecursor (env : Environment) (declName : Name) : Environment :=
   auxRecExt.tag env declName
 
@@ -51,6 +50,7 @@ def isBRecOnRecursor (env : Environment) (declName : Name) : Bool :=
 
 builtin_initialize noConfusionExt : TagDeclarationExtension ← mkTagDeclarationExtension
 
+@[export lean_mark_no_confusion]
 def markNoConfusion (env : Environment) (n : Name) : Environment :=
   noConfusionExt.tag env n
 

src/Lean/BuiltinDocAttr.lean

@@ -5,12 +5,12 @@ Authors: Mario Carneiro
 -/
 prelude
 import Lean.Compiler.InitAttr
-import Lean.DocString.Extension
+import Lean.DocString
 
 namespace Lean
 
 def declareBuiltinDocStringAndRanges (declName : Name) : AttrM Unit := do
-  if let some doc ← findSimpleDocString? (← getEnv) declName (includeBuiltin := false) then
+  if let some doc ← findDocString? (← getEnv) declName (includeBuiltin := false) then
     declareBuiltin (declName ++ `docString) (mkAppN (mkConst ``addBuiltinDocString) #[toExpr declName, toExpr doc])
   if let some declRanges ← findDeclarationRanges? declName then
     declareBuiltin (declName ++ `declRange) (mkAppN (mkConst ``addBuiltinDeclarationRanges) #[toExpr declName, toExpr declRanges])

src/Lean/Compiler/FFI.lean

@@ -18,13 +18,6 @@ private opaque getLeancExtraFlags : Unit → String
 def getCFlags (leanSysroot : FilePath) : Array String :=
   #["-I", (leanSysroot / "include").toString] ++ (getLeancExtraFlags ()).trim.splitOn
 
-@[extern "lean_get_leanc_internal_flags"]
-private opaque getLeancInternalFlags : Unit → String
-
-/-- Return C compiler flags needed to use the C compiler bundled with the Lean toolchain. -/
-def getInternalCFlags (leanSysroot : FilePath) : Array String :=
-  (getLeancInternalFlags ()).trim.splitOn.toArray.map (·.replace "ROOT" leanSysroot.toString)
-
 @[extern "lean_get_linker_flags"]
 private opaque getBuiltinLinkerFlags (linkStatic : Bool) : String
 
@@ -32,11 +25,4 @@ private opaque getBuiltinLinkerFlags (linkStatic : Bool) : String
 def getLinkerFlags (leanSysroot : FilePath) (linkStatic := true) : Array String :=
   #["-L", (leanSysroot / "lib" / "lean").toString] ++ (getBuiltinLinkerFlags linkStatic).trim.splitOn
 
-@[extern "lean_get_internal_linker_flags"]
-private opaque getBuiltinInternalLinkerFlags : Unit → String
-
-/-- Return linker flags needed to use the linker bundled with the Lean toolchain. -/
-def getInternalLinkerFlags (leanSysroot : FilePath) : Array String :=
-  (getBuiltinInternalLinkerFlags ()).trim.splitOn.toArray.map (·.replace "ROOT" leanSysroot.toString)
-
 end Lean.Compiler.FFI

src/Lean/Compiler/IR/EmitC.lean

@@ -499,11 +499,7 @@ def emitLit (z : VarId) (t : IRType) (v : LitVal) : M Unit := do
   emitLhs z;
   match v with
   | LitVal.num v => emitNumLit t v; emitLn ";"
-  | LitVal.str v =>
-    emit "lean_mk_string_unchecked(";
-    emit (quoteString v); emit ", ";
-    emit v.utf8ByteSize; emit ", ";
-    emit v.length; emitLn ");"
+  | LitVal.str v => emit "lean_mk_string_from_bytes("; emit (quoteString v); emit ", "; emit v.utf8ByteSize; emitLn ");"
 
 def emitVDecl (z : VarId) (t : IRType) (v : Expr) : M Unit :=
   match v with

src/Lean/Compiler/IR/EmitLLVM.lean

@@ -178,14 +178,14 @@ def callLeanUnsignedToNatFn (builder : LLVM.Builder llvmctx)
   let nv ← constIntUnsigned n
   LLVM.buildCall2 builder fnty f #[nv] name
 
-def callLeanMkStringUncheckedFn (builder : LLVM.Builder llvmctx)
-    (strPtr nBytes nChars : LLVM.Value llvmctx) (name : String) : M llvmctx (LLVM.Value llvmctx) := do
-  let fnName :=  "lean_mk_string_unchecked"
+def callLeanMkStringFromBytesFn (builder : LLVM.Builder llvmctx)
+    (strPtr nBytes : LLVM.Value llvmctx) (name : String) : M llvmctx (LLVM.Value llvmctx) := do
+  let fnName :=  "lean_mk_string_from_bytes"
   let retty ← LLVM.voidPtrType llvmctx
-  let argtys :=  #[← LLVM.voidPtrType llvmctx, ← LLVM.size_tType llvmctx, ← LLVM.size_tType llvmctx]
+  let argtys :=  #[← LLVM.voidPtrType llvmctx, ← LLVM.size_tType llvmctx]
   let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys
   let fnty ← LLVM.functionType retty argtys
-  LLVM.buildCall2 builder fnty fn #[strPtr, nBytes, nChars] name
+  LLVM.buildCall2 builder fnty fn #[strPtr, nBytes] name
 
 def callLeanMkString (builder : LLVM.Builder llvmctx)
     (strPtr : LLVM.Value llvmctx) (name : String) : M llvmctx (LLVM.Value llvmctx) := do
@@ -772,8 +772,7 @@ def emitLit (builder : LLVM.Builder llvmctx)
                                 (← LLVM.opaquePointerTypeInContext llvmctx)
                                 str_global #[zero] ""
                  let nbytes ← constIntSizeT v.utf8ByteSize
-                 let nchars ← constIntSizeT v.length
-                 callLeanMkStringUncheckedFn builder strPtr nbytes nchars ""
+                 callLeanMkStringFromBytesFn builder strPtr nbytes ""
   LLVM.buildStore builder zv zslot
   return zslot
 

src/Lean/CoreM.lean

@@ -472,30 +472,23 @@ def Exception.isInterrupt : Exception → Bool
 
 /--
 Custom `try-catch` for all monads based on `CoreM`. We usually don't want to catch "runtime
-exceptions" these monads, but on `CommandElabM` or, in specific cases, using `tryCatchRuntimeEx`.
-See issues #2775 and #2744 as well as `MonadAlwaysExcept`. Also, we never want to catch interrupt
-exceptions inside the elaborator.
+exceptions" these monads, but on `CommandElabM`. See issues #2775 and #2744 as well as
+`MonadAlwaysExcept`. Also, we never want to catch interrupt exceptions inside the elaborator.
 -/
 @[inline] protected def Core.tryCatch (x : CoreM α) (h : Exception → CoreM α) : CoreM α := do
   try
     x
   catch ex =>
     if ex.isInterrupt || ex.isRuntime then
-      throw ex
+
+      throw ex -- We should use `tryCatchRuntimeEx` for catching runtime exceptions
     else
       h ex
 
-/--
-A variant of `tryCatch` that also catches runtime exception (see also `tryCatch` documentation).
-Like `tryCatch`, this function does not catch interrupt exceptions, which are not considered runtime
-exceptions.
--/
 @[inline] protected def Core.tryCatchRuntimeEx (x : CoreM α) (h : Exception → CoreM α) : CoreM α := do
   try
     x
   catch ex =>
-    if ex.isInterrupt then
-      throw ex
     h ex
 
 instance : MonadExceptOf Exception CoreM where

src/Lean/Data/HashMap.lean

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

src/Lean/Data/PersistentArray.lean

@@ -72,6 +72,8 @@ def get! [Inhabited α] (t : PersistentArray α) (i : Nat) : α :=
 instance [Inhabited α] : GetElem (PersistentArray α) Nat α fun as i => i < as.size where
   getElem xs i _ := xs.get! i
 
+instance [Inhabited α] : LawfulGetElem (PersistentArray α) Nat α fun as i => i < as.size where
+
 partial def setAux : PersistentArrayNode α → USize → USize → α → PersistentArrayNode α
   | node cs, i, shift, a =>
     let j     := div2Shift i shift

src/Lean/Data/PersistentHashMap.lean

@@ -23,13 +23,6 @@ inductive Node (α : Type u) (β : Type v) : Type (max u v) where
   | entries   (es : Array (Entry α β (Node α β))) : Node α β
   | collision (ks : Array α) (vs : Array β) (h : ks.size = vs.size) : Node α β
 
-partial def Node.isEmpty : Node α β → Bool
-  | .collision .. => false
-  | .entries es => es.all fun
-    | .entry .. => false
-    | .ref n    => n.isEmpty
-    | .null     => true
-
 instance {α β} : Inhabited (Node α β) := ⟨Node.entries #[]⟩
 
 abbrev shift         : USize  := 5
@@ -43,7 +36,8 @@ def mkEmptyEntriesArray {α β} : Array (Entry α β (Node α β)) :=
 end PersistentHashMap
 
 structure PersistentHashMap (α : Type u) (β : Type v) [BEq α] [Hashable α] where
-  root : PersistentHashMap.Node α β := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray
+  root    : PersistentHashMap.Node α β := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray
+  size    : Nat                        := 0
 
 abbrev PHashMap (α : Type u) (β : Type v) [BEq α] [Hashable α] := PersistentHashMap α β
 
@@ -51,8 +45,8 @@ namespace PersistentHashMap
 
 def empty [BEq α] [Hashable α] : PersistentHashMap α β := {}
 
-def isEmpty {_ : BEq α} {_ : Hashable α} : PersistentHashMap α β → Bool
-  | { root } => root.isEmpty
+def isEmpty [BEq α] [Hashable α] (m : PersistentHashMap α β) : Bool :=
+  m.size == 0
 
 instance [BEq α] [Hashable α] : Inhabited (PersistentHashMap α β) := ⟨{}⟩
 
@@ -136,7 +130,7 @@ partial def insertAux [BEq α] [Hashable α] : Node α β → USize → USize
         else Entry.ref $ mkCollisionNode k' v' k v
 
 def insert {_ : BEq α} {_ : Hashable α} : PersistentHashMap α β → α → β → PersistentHashMap α β
-  | { root }, k, v => { root := insertAux root (hash k |>.toUSize) 1 k v }
+  | { root := n, size := sz }, k, v => { root := insertAux n (hash k |>.toUSize) 1 k v, size := sz + 1 }
 
 partial def findAtAux [BEq α] (keys : Array α) (vals : Array β) (heq : keys.size = vals.size) (i : Nat) (k : α) : Option β :=
   if h : i < keys.size then
@@ -156,11 +150,13 @@ partial def findAux [BEq α] : Node α β → USize → α → Option β
   | Node.collision keys vals heq, _, k => findAtAux keys vals heq 0 k
 
 def find? {_ : BEq α} {_ : Hashable α} : PersistentHashMap α β → α → Option β
-  | { root }, k => findAux root (hash k |>.toUSize) k
+  | { root := n, .. }, k => findAux n (hash k |>.toUSize) k
 
 instance {_ : BEq α} {_ : Hashable α} : GetElem (PersistentHashMap α β) α (Option β) fun _ _ => True where
   getElem m i _ := m.find? i
 
+instance {_ : BEq α} {_ : Hashable α} : LawfulGetElem (PersistentHashMap α β) α (Option β) fun _ _ => True where
+
 @[inline] def findD {_ : BEq α} {_ : Hashable α} (m : PersistentHashMap α β) (a : α) (b₀ : β) : β :=
   (m.find? a).getD b₀
 
@@ -187,7 +183,7 @@ partial def findEntryAux [BEq α] : Node α β → USize → α → Option (α
   | Node.collision keys vals heq, _, k => findEntryAtAux keys vals heq 0 k
 
 def findEntry? {_ : BEq α} {_ : Hashable α} : PersistentHashMap α β → α → Option (α × β)
-  | { root }, k => findEntryAux root (hash k |>.toUSize) k
+  | { root := n, .. }, k => findEntryAux n (hash k |>.toUSize) k
 
 partial def containsAtAux [BEq α] (keys : Array α) (vals : Array β) (heq : keys.size = vals.size) (i : Nat) (k : α) : Bool :=
   if h : i < keys.size then
@@ -206,7 +202,7 @@ partial def containsAux [BEq α] : Node α β → USize → α → Bool
   | Node.collision keys vals heq, _, k => containsAtAux keys vals heq 0 k
 
 def contains [BEq α] [Hashable α] : PersistentHashMap α β → α → Bool
-  | { root }, k => containsAux root (hash k |>.toUSize) k
+  | { root := n, .. }, k => containsAux n (hash k |>.toUSize) k
 
 partial def isUnaryEntries (a : Array (Entry α β (Node α β))) (i : Nat) (acc : Option (α × β)) : Option (α × β) :=
   if h : i < a.size then
@@ -229,7 +225,7 @@ def isUnaryNode : Node α β → Option (α × β)
     else
       none
 
-partial def eraseAux [BEq α] : Node α β → USize → α → Node α β
+partial def eraseAux [BEq α] : Node α β → USize → α → Node α β × Bool
   | n@(Node.collision keys vals heq), _, k =>
     match keys.indexOf? k with
     | some idx =>
@@ -238,26 +234,28 @@ partial def eraseAux [BEq α] : Node α β → USize → α → Node α β
       let vals' := vals.feraseIdx (Eq.ndrec idx heq)
       have veq := vals.size_feraseIdx (Eq.ndrec idx heq)
       have : keys.size - 1 = vals.size - 1 := by rw [heq]
-      Node.collision keys' vals' (keq.trans (this.trans veq.symm))
-    | none     => n
+      (Node.collision keys' vals' (keq.trans (this.trans veq.symm)), true)
+    | none     => (n, false)
   | n@(Node.entries entries), h, k =>
     let j       := (mod2Shift h shift).toNat
     let entry   := entries.get! j
     match entry with
-    | Entry.null       => n
+    | Entry.null       => (n, false)
     | Entry.entry k' _ =>
-      if k == k' then Node.entries (entries.set! j Entry.null) else n
+      if k == k' then (Node.entries (entries.set! j Entry.null), true) else (n, false)
     | Entry.ref node   =>
       let entries := entries.set! j Entry.null
-      let newNode := eraseAux node (div2Shift h shift) k
-      match isUnaryNode newNode with
-      | none        => Node.entries (entries.set! j (Entry.ref newNode))
-      | some (k, v) => Node.entries (entries.set! j (Entry.entry k v))
+      let (newNode, deleted) := eraseAux node (div2Shift h shift) k
+      if !deleted then (n, false)
+      else match isUnaryNode newNode with
+        | none        => (Node.entries (entries.set! j (Entry.ref newNode)), true)
+        | some (k, v) => (Node.entries (entries.set! j (Entry.entry k v)), true)
 
 def erase {_ : BEq α} {_ : Hashable α} : PersistentHashMap α β → α → PersistentHashMap α β
-  | { root }, k =>
+  | { root := n, size := sz }, k =>
     let h := hash k |>.toUSize
-    { root := eraseAux root h k }
+    let (n, del) := eraseAux n h k
+    { root := n, size := if del then sz - 1 else sz }
 
 section
 variable {m : Type w → Type w'} [Monad m]
@@ -319,7 +317,7 @@ partial def mapMAux {α : Type u} {β : Type v} {σ : Type u} {m : Type u → Ty
 
 def mapM {α : Type u} {β : Type v} {σ : Type u} {m : Type u → Type w} [Monad m] {_ : BEq α} {_ : Hashable α} (pm : PersistentHashMap α β) (f : β → m σ) : m (PersistentHashMap α σ) := do
   let root ← mapMAux f pm.root
-  return { root }
+  return { pm with root }
 
 def map {α : Type u} {β : Type v} {σ : Type u} {_ : BEq α} {_ : Hashable α} (pm : PersistentHashMap α β) (f : β → σ) : PersistentHashMap α σ :=
   Id.run <| pm.mapM f

src/Lean/Data/PersistentHashSet.lean

@@ -44,6 +44,9 @@ variable {_ : BEq α} {_ : Hashable α}
 @[inline] def contains (s : PersistentHashSet α) (a : α) : Bool :=
   s.set.contains a
 
+@[inline] def size (s : PersistentHashSet α) : Nat :=
+  s.set.size
+
 @[inline] def foldM {β : Type v} {m : Type v → Type v} [Monad m] (f : β → α → m β) (init : β) (s : PersistentHashSet α) : m β :=
   s.set.foldlM (init := init) fun d a _ => f d a
 

src/Lean/Data/SMap.lean

@@ -90,6 +90,12 @@ def switch (m : SMap α β) : SMap α β :=
 def fold {σ : Type w} (f : σ → α → β → σ) (init : σ) (m : SMap α β) : σ :=
   m.map₂.foldl f $ m.map₁.fold f init
 
+def size (m : SMap α β) : Nat :=
+  m.map₁.size + m.map₂.size
+
+def stageSizes (m : SMap α β) : Nat × Nat :=
+  (m.map₁.size, m.map₂.size)
+
 def numBuckets (m : SMap α β) : Nat :=
   m.map₁.numBuckets
 

src/Lean/Data/SSet.lean

@@ -34,6 +34,9 @@ abbrev switch (s : SSet α) : SSet α :=
 abbrev fold (f : σ → α → σ) (init : σ) (s : SSet α) : σ :=
   SMap.fold (fun d a _ => f d a) init s
 
+abbrev size (s : SSet α) : Nat :=
+  SMap.size s
+
 def toList (m : SSet α) : List α :=
   m.fold (init := []) fun es a => a::es
 

src/Lean/Declaration.lean

@@ -35,7 +35,7 @@ inductive ReducibilityHints where
   | opaque  : ReducibilityHints
   | abbrev  : ReducibilityHints
   | regular : UInt32 → ReducibilityHints
-  deriving Inhabited, BEq
+  deriving Inhabited
 
 @[export lean_mk_reducibility_hints_regular]
 def mkReducibilityHintsRegularEx (h : UInt32) : ReducibilityHints :=
@@ -117,7 +117,7 @@ structure DefinitionVal extends ConstantVal where
     are compiled using recursors and `WellFounded.fix`.
   -/
   all : List Name := [name]
-  deriving Inhabited, BEq
+  deriving Inhabited
 
 @[export lean_mk_definition_val]
 def mkDefinitionValEx (name : Name) (levelParams : List Name) (type : Expr) (value : Expr) (hints : ReducibilityHints) (safety : DefinitionSafety) (all : List Name) : DefinitionVal := {
@@ -161,13 +161,13 @@ def mkOpaqueValEx (name : Name) (levelParams : List Name) (type : Expr) (value :
 structure Constructor where
   name : Name
   type : Expr
-  deriving Inhabited, BEq
+  deriving Inhabited
 
 structure InductiveType where
   name : Name
   type : Expr
   ctors : List Constructor
-  deriving Inhabited, BEq
+  deriving Inhabited
 
 /-- Declaration object that can be sent to the kernel. -/
 inductive Declaration where
@@ -178,7 +178,7 @@ inductive Declaration where
   | quotDecl
   | mutualDefnDecl  (defns : List DefinitionVal) -- All definitions must be marked as `unsafe` or `partial`
   | inductDecl      (lparams : List Name) (nparams : Nat) (types : List InductiveType) (isUnsafe : Bool)
-  deriving Inhabited, BEq
+  deriving Inhabited
 
 @[export lean_mk_inductive_decl]
 def mkInductiveDeclEs (lparams : List Name) (nparams : Nat) (types : List InductiveType) (isUnsafe : Bool) : Declaration :=
@@ -189,10 +189,6 @@ def Declaration.isUnsafeInductiveDeclEx : Declaration → Bool
   | Declaration.inductDecl _ _ _ isUnsafe => isUnsafe
   | _ => false
 
-def Declaration.definitionVal! : Declaration → DefinitionVal
-  | .defnDecl val => val
-  | _ => panic! "Expected a `Declaration.defnDecl`."
-
 @[specialize] def Declaration.foldExprM {α} {m : Type → Type} [Monad m] (d : Declaration) (f : α → Expr → m α) (a : α) : m α :=
   match d with
   | Declaration.quotDecl                                        => pure a

src/Lean/DocString.lean

@@ -4,26 +4,58 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Lean.DocString.Extension
-import Lean.Parser.Tactic.Doc
-
-set_option linter.missingDocs true
-
--- This module contains the main query interface for docstrings, which assembles user-visible
--- docstrings.
--- The module `Lean.DocString.Extension` contains the underlying data.
+import Lean.DeclarationRange
+import Lean.MonadEnv
+import Init.Data.String.Extra
 
 namespace Lean
-open Lean.Parser.Tactic.Doc
 
-/--
-Finds the docstring for a name, taking tactic alternate forms and documentation extensions into
-account.
+private builtin_initialize builtinDocStrings : IO.Ref (NameMap String) ← IO.mkRef {}
+private builtin_initialize docStringExt : MapDeclarationExtension String ← mkMapDeclarationExtension
 
-Use `Lean.findSimpleDocString?` to look up the raw docstring without resolving alternate forms or
-including extensions.
--/
-def findDocString? (env : Environment) (declName : Name) (includeBuiltin := true) : IO (Option String) := do
-  let declName := alternativeOfTactic env declName |>.getD declName
-  let exts := getTacticExtensionString env declName
-  return (← findSimpleDocString? env declName (includeBuiltin := includeBuiltin)).map (· ++ exts)
+def addBuiltinDocString (declName : Name) (docString : String) : IO Unit :=
+  builtinDocStrings.modify (·.insert declName docString.removeLeadingSpaces)
+
+def addDocString [Monad m] [MonadError m] [MonadEnv m] (declName : Name) (docString : String) : m Unit := do
+  unless (← getEnv).getModuleIdxFor? declName |>.isNone do
+    throwError s!"invalid doc string, declaration '{declName}' is in an imported module"
+  modifyEnv fun env => docStringExt.insert env declName docString.removeLeadingSpaces
+
+def addDocString' [Monad m] [MonadError m] [MonadEnv m] (declName : Name) (docString? : Option String) : m Unit :=
+  match docString? with
+  | some docString => addDocString declName docString
+  | none => return ()
+
+def findDocString? (env : Environment) (declName : Name) (includeBuiltin := true) : IO (Option String) :=
+  if let some docStr := docStringExt.find? env declName then
+    return some docStr
+  else if includeBuiltin then
+    return (← builtinDocStrings.get).find? declName
+  else
+    return none
+
+structure ModuleDoc where
+  doc : String
+  declarationRange : DeclarationRange
+
+private builtin_initialize moduleDocExt : SimplePersistentEnvExtension ModuleDoc (PersistentArray ModuleDoc) ← registerSimplePersistentEnvExtension {
+  addImportedFn := fun _ => {}
+  addEntryFn    := fun s e => s.push e
+  toArrayFn     := fun es => es.toArray
+}
+
+def addMainModuleDoc (env : Environment) (doc : ModuleDoc) : Environment :=
+  moduleDocExt.addEntry env doc
+
+def getMainModuleDoc (env : Environment) : PersistentArray ModuleDoc :=
+  moduleDocExt.getState env
+
+def getModuleDoc? (env : Environment) (moduleName : Name) : Option (Array ModuleDoc) :=
+  env.getModuleIdx? moduleName |>.map fun modIdx => moduleDocExt.getModuleEntries env modIdx
+
+def getDocStringText [Monad m] [MonadError m] [MonadRef m] (stx : TSyntax `Lean.Parser.Command.docComment) : m String :=
+  match stx.raw[1] with
+  | Syntax.atom _ val => return val.extract 0 (val.endPos - ⟨2⟩)
+  | _                 => throwErrorAt stx "unexpected doc string{indentD stx.raw[1]}"
+
+end Lean

src/Lean/DocString/Extension.lean

@@ -1,69 +0,0 @@
-/-
-Copyright (c) 2021 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import Lean.DeclarationRange
-import Lean.MonadEnv
-import Init.Data.String.Extra
-
--- This module contains the underlying data for docstrings, with as few imports as possible, so that
--- docstrings can be saved in as much of the compiler as possible.
--- The module `Lean.DocString` contains the query interface, which needs to look at additional data
--- to construct user-visible docstrings.
-
-namespace Lean
-
-private builtin_initialize builtinDocStrings : IO.Ref (NameMap String) ← IO.mkRef {}
-private builtin_initialize docStringExt : MapDeclarationExtension String ← mkMapDeclarationExtension
-
-def addBuiltinDocString (declName : Name) (docString : String) : IO Unit :=
-  builtinDocStrings.modify (·.insert declName docString.removeLeadingSpaces)
-
-def addDocString [Monad m] [MonadError m] [MonadEnv m] (declName : Name) (docString : String) : m Unit := do
-  unless (← getEnv).getModuleIdxFor? declName |>.isNone do
-    throwError s!"invalid doc string, declaration '{declName}' is in an imported module"
-  modifyEnv fun env => docStringExt.insert env declName docString.removeLeadingSpaces
-
-def addDocString' [Monad m] [MonadError m] [MonadEnv m] (declName : Name) (docString? : Option String) : m Unit :=
-  match docString? with
-  | some docString => addDocString declName docString
-  | none => return ()
-
-/--
-Finds a docstring without performing any alias resolution or enrichment with extra metadata.
-
-Docstrings to be shown to a user should be looked up with `Lean.findDocString?` instead.
--/
-def findSimpleDocString? (env : Environment) (declName : Name) (includeBuiltin := true) : IO (Option String) :=
-  if let some docStr := docStringExt.find? env declName then
-    return some docStr
-  else if includeBuiltin then
-    return (← builtinDocStrings.get).find? declName
-  else
-    return none
-
-structure ModuleDoc where
-  doc : String
-  declarationRange : DeclarationRange
-
-private builtin_initialize moduleDocExt : SimplePersistentEnvExtension ModuleDoc (PersistentArray ModuleDoc) ← registerSimplePersistentEnvExtension {
-  addImportedFn := fun _ => {}
-  addEntryFn    := fun s e => s.push e
-  toArrayFn     := fun es => es.toArray
-}
-
-def addMainModuleDoc (env : Environment) (doc : ModuleDoc) : Environment :=
-  moduleDocExt.addEntry env doc
-
-def getMainModuleDoc (env : Environment) : PersistentArray ModuleDoc :=
-  moduleDocExt.getState env
-
-def getModuleDoc? (env : Environment) (moduleName : Name) : Option (Array ModuleDoc) :=
-  env.getModuleIdx? moduleName |>.map fun modIdx => moduleDocExt.getModuleEntries env modIdx
-
-def getDocStringText [Monad m] [MonadError m] (stx : TSyntax `Lean.Parser.Command.docComment) : m String :=
-  match stx.raw[1] with
-  | Syntax.atom _ val => return val.extract 0 (val.endPos - ⟨2⟩)
-  | _                 => throwErrorAt stx "unexpected doc string{indentD stx.raw[1]}"

src/Lean/Elab.lean

@@ -50,4 +50,3 @@ import Lean.Elab.ParseImportsFast
 import Lean.Elab.GuardMsgs
 import Lean.Elab.CheckTactic
 import Lean.Elab.MatchExpr
-import Lean.Elab.Tactic.Doc

src/Lean/Elab/Attributes.lean

@@ -39,7 +39,7 @@ def toAttributeKind (attrKindStx : Syntax) : MacroM AttributeKind := do
 def mkAttrKindGlobal : Syntax :=
   mkNode ``Lean.Parser.Term.attrKind #[mkNullNode]
 
-def elabAttr [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLiftT IO m] (attrInstance : Syntax) : m Attribute := do
+def elabAttr [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadInfoTree m] [MonadLiftT IO m] (attrInstance : Syntax) : m Attribute := do
   /- attrInstance     := ppGroup $ leading_parser attrKind >> attrParser -/
   let attrKind ← liftMacroM <| toAttributeKind attrInstance[0]
   let attr := attrInstance[1]
@@ -55,7 +55,7 @@ def elabAttr [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMa
      So, we expand them before here before we invoke the attributer handlers implemented using `AttrM`. -/
   return { kind := attrKind, name := attrName, stx := attr }
 
-def elabAttrs [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLog m] [MonadLiftT IO m] (attrInstances : Array Syntax) : m (Array Attribute) := do
+def elabAttrs [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLog m] [MonadInfoTree m] [MonadLiftT IO m] (attrInstances : Array Syntax) : m (Array Attribute) := do
   let mut attrs := #[]
   for attr in attrInstances do
     try
@@ -65,7 +65,7 @@ def elabAttrs [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadM
   return attrs
 
 -- leading_parser "@[" >> sepBy1 attrInstance ", " >> "]"
-def elabDeclAttrs [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLog m] [MonadLiftT IO m] (stx : Syntax) : m (Array Attribute) :=
+def elabDeclAttrs [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLog m] [MonadInfoTree m] [MonadLiftT IO m] (stx : Syntax) : m (Array Attribute) :=
   elabAttrs stx[1].getSepArgs
 
 end Lean.Elab

src/Lean/Elab/BuiltinCommand.lean

@@ -262,22 +262,16 @@ def elabCheckCore (ignoreStuckTC : Bool) : CommandElab
 
 @[builtin_command_elab Lean.Parser.Command.check] def elabCheck : CommandElab := elabCheckCore (ignoreStuckTC := true)
 
-@[builtin_command_elab Lean.reduceCmd] def elabReduce : CommandElab
-  | `(#reduce%$tk $term) => go tk term
-  | `(#reduce%$tk (proofs := true) $term) => go tk term (skipProofs := false)
-  | `(#reduce%$tk (types := true) $term) => go tk term (skipTypes := false)
-  | `(#reduce%$tk (proofs := true) (types := true) $term) => go tk term (skipProofs := false) (skipTypes := false)
+@[builtin_command_elab Lean.Parser.Command.reduce] def elabReduce : CommandElab
+  | `(#reduce%$tk $term) => withoutModifyingEnv <| runTermElabM fun _ => Term.withDeclName `_reduce do
+    let e ← Term.elabTerm term none
+    Term.synthesizeSyntheticMVarsNoPostponing
+    let e ← Term.levelMVarToParam (← instantiateMVars e)
+    -- TODO: add options or notation for setting the following parameters
+    withTheReader Core.Context (fun ctx => { ctx with options := ctx.options.setBool `smartUnfolding false }) do
+      let e ← withTransparency (mode := TransparencyMode.all) <| reduce e (skipProofs := false) (skipTypes := false)
+      logInfoAt tk e
   | _ => throwUnsupportedSyntax
-where
-  go (tk : Syntax) (term : Syntax) (skipProofs := true) (skipTypes := true) : CommandElabM Unit :=
-    withoutModifyingEnv <| runTermElabM fun _ => Term.withDeclName `_reduce do
-      let e ← Term.elabTerm term none
-      Term.synthesizeSyntheticMVarsNoPostponing
-      let e ← Term.levelMVarToParam (← instantiateMVars e)
-      -- TODO: add options or notation for setting the following parameters
-      withTheReader Core.Context (fun ctx => { ctx with options := ctx.options.setBool `smartUnfolding false }) do
-        let e ← withTransparency (mode := TransparencyMode.all) <| reduce e (skipProofs := skipProofs) (skipTypes := skipTypes)
-        logInfoAt tk e
 
 def hasNoErrorMessages : CommandElabM Bool := do
   return !(← get).messages.hasErrors

src/Lean/Elab/BuiltinTerm.lean

@@ -157,19 +157,9 @@ private def mkTacticMVar (type : Expr) (tacticCode : Syntax) : TermElabM Expr :=
   registerSyntheticMVar ref mvarId <| SyntheticMVarKind.tactic tacticCode (← saveContext)
   return mvar
 
-register_builtin_option debug.byAsSorry : Bool := {
-  defValue := false
-  group    := "debug"
-  descr    := "replace `by ..` blocks with `sorry` IF the expected type is a proposition"
-}
-
 @[builtin_term_elab byTactic] def elabByTactic : TermElab := fun stx expectedType? => do
   match expectedType? with
-  | some expectedType =>
-    if ← pure (debug.byAsSorry.get (← getOptions)) <&&> isProp expectedType then
-      mkSorry expectedType false
-    else
-      mkTacticMVar expectedType stx
+  | some expectedType => mkTacticMVar expectedType stx
   | none =>
     tryPostpone
     throwError ("invalid 'by' tactic, expected type has not been provided")

src/Lean/Elab/CheckTactic.lean

@@ -17,7 +17,6 @@ namespace Lean.Elab.CheckTactic
 
 open Lean.Meta CheckTactic
 open Lean.Elab.Tactic
-open Lean.Elab.Term
 open Lean.Elab.Command
 
 @[builtin_command_elab Lean.Parser.checkTactic]
@@ -25,7 +24,7 @@ def elabCheckTactic : CommandElab := fun stx => do
   let `(#check_tactic $t ~> $result by $tac) := stx | throwUnsupportedSyntax
   withoutModifyingEnv $ do
     runTermElabM $ fun _vars => do
-      let u ← withSynthesize (postpone := .no) <| Lean.Elab.Term.elabTerm t none
+      let u ← Lean.Elab.Term.elabTerm t none
       let type ← inferType u
       let checkGoalType ← mkCheckGoalType u type
       let mvar ← mkFreshExprMVar (.some checkGoalType)

src/Lean/Elab/Command.lean

@@ -81,10 +81,7 @@ Remark: see comment at TermElabM
 @[always_inline]
 instance : Monad CommandElabM := let i := inferInstanceAs (Monad CommandElabM); { pure := i.pure, bind := i.bind }
 
-/--
-Like `Core.tryCatchRuntimeEx`; runtime errors are generally used to abort term elaboration, so we do
-want to catch and process them at the command level.
--/
+/-- Like `Core.tryCatch` but do catch runtime exceptions. -/
 @[inline] protected def tryCatch (x : CommandElabM α) (h : Exception → CommandElabM α) :
     CommandElabM α := do
   try

src/Lean/Elab/DeclModifiers.lean

@@ -81,14 +81,10 @@ def Modifiers.isNonrec : Modifiers → Bool
   | { recKind := .nonrec, .. } => true
   | _                          => false
 
-/-- Adds attribute `attr` in `modifiers` -/
-def Modifiers.addAttr (modifiers : Modifiers) (attr : Attribute) : Modifiers :=
+/-- Store `attr` in `modifiers` -/
+def Modifiers.addAttribute (modifiers : Modifiers) (attr : Attribute) : Modifiers :=
   { modifiers with attrs := modifiers.attrs.push attr }
 
-/-- Filters attributes using `p` -/
-def Modifiers.filterAttrs (modifiers : Modifiers) (p : Attribute → Bool) : Modifiers :=
-  { modifiers with attrs := modifiers.attrs.filter p }
-
 instance : ToFormat Modifiers := ⟨fun m =>
   let components : List Format :=
     (match m.docString? with

src/Lean/Elab/Declaration.lean

@@ -184,7 +184,7 @@ def elabInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit :=
   elabInductiveViews #[v]
 
 def elabClassInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
-  let modifiers := modifiers.addAttr { name := `class }
+  let modifiers := modifiers.addAttribute { name := `class }
   let v ← classInductiveSyntaxToView modifiers stx
   elabInductiveViews #[v]
 

src/Lean/Elab/DefView.lean

@@ -135,8 +135,8 @@ open Meta
 def mkDefViewOfAbbrev (modifiers : Modifiers) (stx : Syntax) : DefView :=
   -- leading_parser "abbrev " >> declId >> optDeclSig >> declVal
   let (binders, type) := expandOptDeclSig stx[2]
-  let modifiers       := modifiers.addAttr { name := `inline }
-  let modifiers       := modifiers.addAttr { name := `reducible }
+  let modifiers       := modifiers.addAttribute { name := `inline }
+  let modifiers       := modifiers.addAttribute { name := `reducible }
   { ref := stx, headerRef := mkNullNode stx.getArgs[:3], kind := DefKind.abbrev, modifiers,
     declId := stx[1], binders, type? := type, value := stx[3] }
 
@@ -159,7 +159,7 @@ def mkDefViewOfInstance (modifiers : Modifiers) (stx : Syntax) : CommandElabM De
   let prio            ← liftMacroM <| expandOptNamedPrio stx[2]
   let attrStx         ← `(attr| instance $(quote prio):num)
   let (binders, type) := expandDeclSig stx[4]
-  let modifiers       := modifiers.addAttr { kind := attrKind, name := `instance, stx := attrStx }
+  let modifiers       := modifiers.addAttribute { kind := attrKind, name := `instance, stx := attrStx }
   let declId ← match stx[3].getOptional? with
     | some declId =>
       if ← isTracingEnabledFor `Elab.instance.mkInstanceName then

src/Lean/Elab/InheritDoc.lean

@@ -5,7 +5,7 @@ Authors: Mario Carneiro
 -/
 prelude
 import Lean.Elab.InfoTree.Main
-import Lean.DocString.Extension
+import Lean.DocString
 
 namespace Lean
 
@@ -21,9 +21,9 @@ builtin_initialize
         let some id := id?
           | throwError "invalid `[inherit_doc]` attribute, could not infer doc source"
         let declName ← Elab.realizeGlobalConstNoOverloadWithInfo id
-        if (← findSimpleDocString? (← getEnv) decl).isSome then
+        if (← findDocString? (← getEnv) decl).isSome then
           logWarning m!"{← mkConstWithLevelParams decl} already has a doc string"
-        let some doc ← findSimpleDocString? (← getEnv) declName
+        let some doc ← findDocString? (← getEnv) declName
           | logWarningAt id m!"{← mkConstWithLevelParams declName} does not have a doc string"
         addDocString decl doc
       | _  => throwError "invalid `[inherit_doc]` attribute"

src/Lean/Elab/LetRec.lean

@@ -30,24 +30,20 @@ structure LetRecView where
 
 /-  group ("let " >> nonReservedSymbol "rec ") >> sepBy1 (group (optional «attributes» >> letDecl)) ", " >> "; " >> termParser -/
 private def mkLetRecDeclView (letRec : Syntax) : TermElabM LetRecView := do
-  let mut decls : Array LetRecDeclView := #[]
-  for attrDeclStx in letRec[1][0].getSepArgs do
+  let decls ← letRec[1][0].getSepArgs.mapM fun (attrDeclStx : Syntax) => do
     let docStr? ← expandOptDocComment? attrDeclStx[0]
     let attrOptStx := attrDeclStx[1]
     let attrs ← if attrOptStx.isNone then pure #[] else elabDeclAttrs attrOptStx[0]
     let decl := attrDeclStx[2][0]
     if decl.isOfKind `Lean.Parser.Term.letPatDecl then
       throwErrorAt decl "patterns are not allowed in 'let rec' expressions"
-    else if decl.isOfKind ``Lean.Parser.Term.letIdDecl || decl.isOfKind ``Lean.Parser.Term.letEqnsDecl then
+    else if decl.isOfKind `Lean.Parser.Term.letIdDecl || decl.isOfKind `Lean.Parser.Term.letEqnsDecl then
       let declId := decl[0]
       unless declId.isIdent do
         throwErrorAt declId "'let rec' expressions must be named"
       let shortDeclName := declId.getId
       let currDeclName? ← getDeclName?
       let declName := currDeclName?.getD Name.anonymous ++ shortDeclName
-      if decls.any fun decl => decl.declName == declName then
-        withRef declId do
-          throwError "'{declName}' has already been declared"
       checkNotAlreadyDeclared declName
       applyAttributesAt declName attrs AttributeApplicationTime.beforeElaboration
       addDocString' declName docStr?
@@ -66,10 +62,8 @@ private def mkLetRecDeclView (letRec : Syntax) : TermElabM LetRecView := do
       else
         liftMacroM <| expandMatchAltsIntoMatch decl decl[3]
       let termination ← WF.elabTerminationHints ⟨attrDeclStx[3]⟩
-      decls := decls.push {
-        ref := declId, attrs, shortDeclName, declName,
-        binderIds, type, mvar, valStx, termination
-      }
+      pure { ref := declId, attrs, shortDeclName, declName, binderIds, type, mvar, valStx,
+             termination : LetRecDeclView }
     else
       throwUnsupportedSyntax
   return { decls, body := letRec[3] }

src/Lean/Elab/MutualDef.lean

@@ -846,7 +846,7 @@ private def levelMVarToParamHeaders (views : Array DefView) (headers : Array Def
   let rec process : StateRefT Nat TermElabM (Array DefViewElabHeader) := do
     let mut newHeaders := #[]
     for view in views, header in headers do
-      if ← pure view.kind.isTheorem <||> isProp header.type then
+      if view.kind.isTheorem then
         newHeaders ←
           withLevelNames header.levelNames do
             return newHeaders.push { header with type := (← levelMVarToParam header.type), levelNames := (← getLevelNames) }

src/Lean/Elab/PreDefinition/Basic.lean

@@ -32,9 +32,6 @@ structure PreDefinition where
   termination : WF.TerminationHints
   deriving Inhabited
 
-def PreDefinition.filterAttrs (preDef : PreDefinition) (p : Attribute → Bool) : PreDefinition :=
-  { preDef with modifiers := preDef.modifiers.filterAttrs p }
-
 def instantiateMVarsAtPreDecls (preDefs : Array PreDefinition) : TermElabM (Array PreDefinition) :=
   preDefs.mapM fun preDef => do
     pure { preDef with type := (← instantiateMVars preDef.type), value := (← instantiateMVars preDef.value) }

src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean

@@ -35,61 +35,12 @@ private def hasBadParamDep? (ys : Array Expr) (indParams : Array Expr) : MetaM (
         return some (p, y)
   return none
 
-/--
-Pass to `k` the `RecArgInfo` for the `i`th parameter in the parameter list `xs`. This performs
-various sanity checks on the argument (is it even an inductive type etc).
-Also wraps all errors in a common “argument cannot be used” header
--/
-def withRecArgInfo (numFixed : Nat) (xs : Array Expr) (i : Nat) (k : RecArgInfo → M α) : M α := do
-  mapError
-    (f := fun msg => m!"argument #{i+1} cannot be used for structural recursion{indentD msg}") do
-  if h : i < xs.size then
-    if i < numFixed then
-      throwError "it is unchanged in the recursive calls"
-    let x := xs[i]
-    let localDecl ← getFVarLocalDecl x
-    if localDecl.isLet then
-      throwError "it is a let-binding"
-    let xType ← whnfD localDecl.type
-    matchConstInduct xType.getAppFn (fun _ => throwError "its type is not an inductive") fun indInfo us => do
-    if !(← hasConst (mkBRecOnName indInfo.name)) then
-      throwError "its type does not have a recursor"
-    else if indInfo.isReflexive && !(← hasConst (mkBInductionOnName indInfo.name)) && !(← isInductivePredicate indInfo.name) then
-      throwError "its type is a reflexive inductive, but {mkBInductionOnName indInfo.name} does not exist and it is not an inductive predicate"
-    else
-      let indArgs    := xType.getAppArgs
-      let indParams  := indArgs.extract 0 indInfo.numParams
-      let indIndices := indArgs.extract indInfo.numParams indArgs.size
-      if !indIndices.all Expr.isFVar then
-        throwError "its type is an inductive family and indices are not variables{indentExpr xType}"
-      else if !indIndices.allDiff then
-        throwError " its type is an inductive family and indices are not pairwise distinct{indentExpr xType}"
-      else
-        let indexMinPos := getIndexMinPos xs indIndices
-        let numFixed    := if indexMinPos < numFixed then indexMinPos else numFixed
-        let fixedParams := xs.extract 0 numFixed
-        let ys          := xs.extract numFixed xs.size
-        match (← hasBadIndexDep? ys indIndices) with
-        | some (index, y) =>
-          throwError "its type is an inductive family{indentExpr xType}\nand index{indentExpr index}\ndepends on the non index{indentExpr y}"
-        | none =>
-          match (← hasBadParamDep? ys indParams) with
-          | some (indParam, y) =>
-            throwError "its type is an inductive datatype{indentExpr xType}\nand parameter{indentExpr indParam}\ndepends on{indentExpr y}"
-          | none =>
-            let indicesPos := indIndices.map fun index => match ys.indexOf? index with | some i => i.val | none => unreachable!
-            k { fixedParams := fixedParams
-                ys          := ys
-                pos         := i - fixedParams.size
-                indicesPos  := indicesPos
-                indName     := indInfo.name
-                indLevels   := us
-                indParams   := indParams
-                indIndices  := indIndices
-                reflexive   := indInfo.isReflexive
-                indPred     := ←isInductivePredicate indInfo.name }
-    else
-      throwError "the index #{i+1} exceeds {xs.size}, the number of parameters"
+private def throwStructuralFailed : MetaM α :=
+  throwError "structural recursion cannot be used"
+
+private def orelse' (x y : M α) : M α := do
+  let saveState ← get
+  orelseMergeErrors x (do set saveState; y)
 
 /--
   Try to find an argument that is structurally smaller in every recursive application.
@@ -98,10 +49,16 @@ def withRecArgInfo (numFixed : Nat) (xs : Array Expr) (i : Nat) (k : RecArgInfo
   We give preference for arguments that are *not* indices of inductive types of other arguments.
   See issue #837 for an example where we can show termination using the index of an inductive family, but
   we don't get the desired definitional equalities.
+
+  We perform two passes. In the first-pass, we only consider arguments that are not indices.
+  In the second pass, we consider them.
+
+  TODO: explore whether there are better solutions, and whether there are other ways to break the heuristic used
+  for creating the smart unfolding auxiliary definition.
 -/
 partial def findRecArg (numFixed : Nat) (xs : Array Expr) (k : RecArgInfo → M α) : M α := do
   /- Collect arguments that are indices. See comment above. -/
-  let indicesRef : IO.Ref (Array Nat) ← IO.mkRef {}
+  let indicesRef : IO.Ref FVarIdSet ← IO.mkRef {}
   for x in xs do
     let xType ← inferType x
     /- Traverse all sub-expressions in the type of `x` -/
@@ -111,22 +68,75 @@ partial def findRecArg (numFixed : Nat) (xs : Array Expr) (k : RecArgInfo → M
         if info.numIndices > 0 && info.numParams + info.numIndices == e.getAppNumArgs then
           for arg in e.getAppArgs[info.numParams:] do
             forEachExpr arg fun e => do
-              if let .some idx := xs.getIdx? e then
-                indicesRef.modify fun indices => indices.push idx
+              if e.isFVar && xs.any (· == e) then
+                indicesRef.modify fun indices => indices.insert e.fvarId!
   let indices ← indicesRef.get
-  let nonIndices := (Array.range xs.size).filter (fun i => !(indices.contains i))
-  let mut errors : Array MessageData := Array.mkArray xs.size m!""
-  let saveState ← get -- backtrack the state for each argument
-  for i in id (nonIndices ++ indices) do
-    let x := xs[i]!
-    trace[Elab.definition.structural] "findRecArg x: {x}"
-    try
-      set saveState
-      return (← withRecArgInfo numFixed xs i k)
-    catch e => errors := errors.set! i e.toMessageData
-  throwError
-    errors.foldl
-      (init := m!"structural recursion cannot be used:")
-      (f := (· ++ Format.line ++ Format.line ++ .))
+  /- We perform two passes. See comment above. -/
+  let rec go (i : Nat) (firstPass : Bool) : M α := do
+    if h : i < xs.size then
+      let x := xs.get ⟨i, h⟩
+      trace[Elab.definition.structural] "findRecArg x: {x}, firstPass: {firstPass}"
+      let localDecl ← getFVarLocalDecl x
+      if localDecl.isLet then
+        throwStructuralFailed
+      else if firstPass == indices.contains localDecl.fvarId then
+        go (i+1) firstPass
+      else
+        let xType ← whnfD localDecl.type
+        matchConstInduct xType.getAppFn (fun _ => go (i+1) firstPass) fun indInfo us => do
+        if !(← hasConst (mkBRecOnName indInfo.name)) then
+          go (i+1) firstPass
+        else if indInfo.isReflexive && !(← hasConst (mkBInductionOnName indInfo.name)) && !(← isInductivePredicate indInfo.name) then
+          go (i+1) firstPass
+        else
+          let indArgs    := xType.getAppArgs
+          let indParams  := indArgs.extract 0 indInfo.numParams
+          let indIndices := indArgs.extract indInfo.numParams indArgs.size
+          if !indIndices.all Expr.isFVar then
+            orelse'
+              (throwError "argument #{i+1} was not used because its type is an inductive family and indices are not variables{indentExpr xType}")
+              (go (i+1) firstPass)
+          else if !indIndices.allDiff then
+            orelse'
+              (throwError "argument #{i+1} was not used because its type is an inductive family and indices are not pairwise distinct{indentExpr xType}")
+              (go (i+1) firstPass)
+          else
+            let indexMinPos := getIndexMinPos xs indIndices
+            let numFixed    := if indexMinPos < numFixed then indexMinPos else numFixed
+            let fixedParams := xs.extract 0 numFixed
+            let ys          := xs.extract numFixed xs.size
+            match (← hasBadIndexDep? ys indIndices) with
+            | some (index, y) =>
+              orelse'
+                (throwError "argument #{i+1} was not used because its type is an inductive family{indentExpr xType}\nand index{indentExpr index}\ndepends on the non index{indentExpr y}")
+                (go (i+1) firstPass)
+            | none =>
+              match (← hasBadParamDep? ys indParams) with
+              | some (indParam, y) =>
+                orelse'
+                  (throwError "argument #{i+1} was not used because its type is an inductive datatype{indentExpr xType}\nand parameter{indentExpr indParam}\ndepends on{indentExpr y}")
+                  (go (i+1) firstPass)
+              | none =>
+                let indicesPos := indIndices.map fun index => match ys.indexOf? index with | some i => i.val | none => unreachable!
+                orelse'
+                  (mapError
+                    (k { fixedParams := fixedParams
+                         ys          := ys
+                         pos         := i - fixedParams.size
+                         indicesPos  := indicesPos
+                         indName     := indInfo.name
+                         indLevels   := us
+                         indParams   := indParams
+                         indIndices  := indIndices
+                         reflexive := indInfo.isReflexive
+                         indPred := ←isInductivePredicate indInfo.name })
+                    (fun msg => m!"argument #{i+1} was not used for structural recursion{indentD msg}"))
+                  (go (i+1) firstPass)
+    else if firstPass then
+      go (i := numFixed) (firstPass := false)
+    else
+      throwStructuralFailed
+
+  go (i := numFixed) (firstPass := true)
 
 end Lean.Elab.Structural

src/Lean/Elab/PreDefinition/Structural/Main.lean

@@ -66,6 +66,7 @@ private def elimRecursion (preDef : PreDefinition) : M (Nat × PreDefinition) :=
     let numFixed ← getFixedPrefix preDef.declName xs value
     trace[Elab.definition.structural] "numFixed: {numFixed}"
     findRecArg numFixed xs fun recArgInfo => do
+      -- when (recArgInfo.indName == `Nat) throwStructuralFailed -- HACK to skip Nat argument
       let valueNew ← if recArgInfo.indPred then
         mkIndPredBRecOn preDef.declName recArgInfo value
       else

src/Lean/Elab/PreDefinition/WF/Main.lean

@@ -129,15 +129,7 @@ def wfRecursion (preDefs : Array PreDefinition) : TermElabM Unit := do
         eraseRecAppSyntaxExpr value
       /- `mkFix` invokes `decreasing_tactic` which may add auxiliary theorems to the environment. -/
       let value ← unfoldDeclsFrom envNew value
-      let unaryPreDef := { unaryPreDef with value }
-      /-
-      We must remove `implemented_by` attributes from the auxiliary application because
-      this attribute is only relevant for code that is compiled. Moreover, the `[implemented_by <decl>]`
-      attribute would check whether the `unaryPreDef` type matches with `<decl>`'s type, and produce
-      and error. See issue #2899
-      -/
-      let unaryPreDef := unaryPreDef.filterAttrs fun attr => attr.name != `implemented_by
-      return unaryPreDef
+      return { unaryPreDef with value }
   trace[Elab.definition.wf] ">> {preDefNonRec.declName} :=\n{preDefNonRec.value}"
   let preDefs ← preDefs.mapM fun d => eraseRecAppSyntax d
   -- Do not complain if the user sets @[semireducible], which usually is a noop,

src/Lean/Elab/Structure.lean

@@ -878,7 +878,7 @@ def structCtor           := leading_parser try (declModifiers >> ident >> " :: "
 def elabStructure (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
   checkValidInductiveModifier modifiers
   let isClass   := stx[0].getKind == ``Parser.Command.classTk
-  let modifiers := if isClass then modifiers.addAttr { name := `class } else modifiers
+  let modifiers := if isClass then modifiers.addAttribute { name := `class } else modifiers
   let declId    := stx[1]
   let params    := stx[2].getArgs
   let exts      := stx[3]

src/Lean/Elab/SyntheticMVars.lean

@@ -498,7 +498,7 @@ private partial def withSynthesizeImp (k : TermElabM α) (postpone : PostponeBeh
   Execute `k`, and synthesize pending synthetic metavariables created while executing `k` are solved.
   If `mayPostpone == false`, then all of them must be synthesized.
   Remark: even if `mayPostpone == true`, the method still uses `synthesizeUsingDefault` -/
-@[inline] def withSynthesize [MonadFunctorT TermElabM m] (k : m α) (postpone := PostponeBehavior.no) : m α :=
+@[inline] def withSynthesize [MonadFunctorT TermElabM m] [Monad m] (k : m α) (postpone := PostponeBehavior.no) : m α :=
   monadMap (m := TermElabM) (withSynthesizeImp · postpone) k
 
 private partial def withSynthesizeLightImp (k : TermElabM α) : TermElabM α := do
@@ -512,7 +512,7 @@ private partial def withSynthesizeLightImp (k : TermElabM α) : TermElabM α :=
     modify fun s => { s with pendingMVars := s.pendingMVars ++ pendingMVarsSaved }
 
 /-- Similar to `withSynthesize`, but uses `postpone := .true`, does not use use `synthesizeUsingDefault` -/
-@[inline] def withSynthesizeLight [MonadFunctorT TermElabM m] (k : m α) : m α :=
+@[inline] def withSynthesizeLight [MonadFunctorT TermElabM m] [Monad m] (k : m α) : m α :=
   monadMap (m := TermElabM) (withSynthesizeLightImp ·) k
 
 /-- Elaborate `stx`, and make sure all pending synthetic metavariables created while elaborating `stx` are solved. -/

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -199,7 +199,7 @@ def evalTacticCDot : Tactic := fun stx => do
   -- but the token antiquotation does not copy trailing whitespace, leading to
   -- differences in the goal display (#2153)
   let initInfo ← mkInitialTacticInfo stx[0]
-  withCaseRef stx[0] stx[1] <| closeUsingOrAdmit do
+  withRef stx[0] <| closeUsingOrAdmit do
     -- save state before/after entering focus on `·`
     withInfoContext (pure ()) initInfo
     Term.withNarrowedArgTacticReuse (argIdx := 1) evalTactic stx

src/Lean/Elab/Tactic/Cache.lean

@@ -37,7 +37,7 @@ private def dbg_cache (msg : String) : TacticM Unit := do
 private def dbg_cache' (cacheRef : IO.Ref Cache) (pos : String.Pos) (mvarId : MVarId) (msg : String) : TacticM Unit := do
   if tactic.dbg_cache.get (← getOptions) then
     let {line, column} := (← getFileMap).toPosition pos
-    dbg_trace "{msg}, line: {line}, column: {column}, contains entry: {(← cacheRef.get).pre.find? { mvarId, pos } |>.isSome}"
+    dbg_trace "{msg}, cache size: {(← cacheRef.get).pre.size}, line: {line}, column: {column}, contains entry: {(← cacheRef.get).pre.find? { mvarId, pos } |>.isSome}"
 
 private def findCache? (cacheRef : IO.Ref Cache) (mvarId : MVarId) (stx : Syntax) (pos : String.Pos) : TacticM (Option Snapshot) := do
   let some s := (← cacheRef.get).pre.find? { mvarId, pos } | do dbg_cache "cache key not found"; return none

src/Lean/Elab/Tactic/Doc.lean

@@ -1,178 +0,0 @@
-/-
-Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: David Thrane Christiansen
--/
-prelude
-import Lean.DocString
-import Lean.Elab.Command
-import Lean.Parser.Tactic.Doc
-import Lean.Parser.Command
-
-namespace Lean.Elab.Tactic.Doc
-open Lean.Parser.Tactic.Doc
-open Lean.Elab.Command
-open Lean.Parser.Command
-
-@[builtin_command_elab «tactic_extension»] def elabTacticExtension : CommandElab
-  | `(«tactic_extension»|tactic_extension%$cmd $_) => do
-    throwErrorAt cmd "Missing documentation comment"
-  | `(«tactic_extension»|$docs:docComment tactic_extension $tac:ident) => do
-    let tacName ← liftTermElabM <| realizeGlobalConstNoOverloadWithInfo tac
-
-    if let some tgt' := alternativeOfTactic (← getEnv) tacName then
-        throwErrorAt tac "'{tacName}' is an alternative form of '{tgt'}'"
-    if !(isTactic (← getEnv) tacName) then
-      throwErrorAt tac "'{tacName}' is not a tactic"
-
-    modifyEnv (tacticDocExtExt.addEntry · (tacName, docs.getDocString))
-    pure ()
-  | _ => throwError "Malformed tactic extension command"
-
-@[builtin_command_elab «register_tactic_tag»] def elabRegisterTacticTag : CommandElab
-  | `(«register_tactic_tag»|$[$doc:docComment]? register_tactic_tag $tag:ident $user:str) => do
-    let docstring ← doc.mapM getDocStringText
-    modifyEnv (knownTacticTagExt.addEntry · (tag.getId, user.getString, docstring))
-  | _ => throwError "Malformed 'register_tactic_tag' command"
-
-/--
-Gets the first string token in a parser description. For example, for a declaration like
-`syntax "squish " term " with " term : tactic`, it returns `some "squish "`, and for a declaration
-like `syntax tactic " <;;;> " tactic : tactic`, it returns `some " <;;;> "`.
-
-Returns `none` for syntax declarations that don't contain a string constant.
--/
-private partial def getFirstTk (e : Expr) : MetaM (Option String) := do
-  match (← Meta.whnf e).getAppFnArgs with
-  | (``ParserDescr.node, #[_, _, p]) => getFirstTk p
-  | (``ParserDescr.trailingNode, #[_, _, _, p]) => getFirstTk p
-  | (``ParserDescr.unary, #[.app _ (.lit (.strVal "withPosition")), p]) => getFirstTk p
-  | (``ParserDescr.unary, #[.app _ (.lit (.strVal "atomic")), p]) => getFirstTk p
-  | (``ParserDescr.binary, #[.app _ (.lit (.strVal "andthen")), p, _]) => getFirstTk p
-  | (``ParserDescr.nonReservedSymbol, #[.lit (.strVal tk), _]) => pure (some tk)
-  | (``ParserDescr.symbol, #[.lit (.strVal tk)]) => pure (some tk)
-  | (``Parser.withAntiquot, #[_, p]) => getFirstTk p
-  | (``Parser.leadingNode, #[_, _, p]) => getFirstTk p
-  | (``HAndThen.hAndThen, #[_, _, _, _, p1, p2]) =>
-    if let some tk ← getFirstTk p1 then pure (some tk)
-    else getFirstTk (.app p2 (.const ``Unit.unit []))
-  | (``Parser.nonReservedSymbol, #[.lit (.strVal tk), _]) => pure (some tk)
-  | (``Parser.symbol, #[.lit (.strVal tk)]) => pure (some tk)
-  | _ => pure none
-
-
-/--
-Creates some `MessageData` for a parser name.
-
-If the parser name maps to a description with an
-identifiable leading token, then that token is shown. Otherwise, the underlying name is shown
-without an `@`. The name includes metadata that makes infoview hovers and the like work. This
-only works for global constants, as the local context is not included.
--/
-private def showParserName (n : Name) : MetaM MessageData := do
-  let env ← getEnv
-  let params :=
-    env.constants.find?' n |>.map (·.levelParams.map Level.param) |>.getD []
-  let tok ←
-    if let some descr := env.find? n |>.bind (·.value?) then
-      if let some tk ← getFirstTk descr then
-        pure <| Std.Format.text tk.trim
-      else pure <| format n
-    else pure <| format n
-  pure <| .ofFormatWithInfos {
-    fmt := "'" ++ .tag 0 tok ++ "'",
-    infos :=
-      .fromList [(0, .ofTermInfo {
-        lctx := .empty,
-        expr := .const n params,
-        stx := .ident .none (toString n).toSubstring n [.decl n []],
-        elaborator := `Delab,
-        expectedType? := none
-      })] _
-  }
-
-
-/--
-Displays all available tactic tags, with documentation.
--/
-@[builtin_command_elab printTacTags] def elabPrintTacTags : CommandElab := fun _stx => do
-  let all :=
-    tacticTagExt.toEnvExtension.getState (← getEnv)
-      |>.importedEntries |>.push (tacticTagExt.exportEntriesFn (tacticTagExt.getState (← getEnv)))
-  let mut mapping : NameMap NameSet := {}
-  for arr in all do
-    for (tac, tag) in arr do
-      mapping := mapping.insert tag (mapping.findD tag {} |>.insert tac)
-
-  let showDocs : Option String → MessageData
-    | none => .nil
-    | some d => Format.line ++ MessageData.joinSep ((d.splitOn "\n").map toMessageData) Format.line
-
-  let showTactics (tag : Name) : MetaM MessageData := do
-    match mapping.find? tag with
-    | none => pure .nil
-    | some tacs =>
-      if tacs.isEmpty then pure .nil
-      else
-        let tacs := tacs.toArray.qsort (·.toString < ·.toString) |>.toList
-        pure (Format.line ++ MessageData.joinSep (← tacs.mapM showParserName) ", ")
-
-  let tagDescrs ← liftTermElabM <| (← allTagsWithInfo).mapM fun (name, userName, docs) => do
-    pure <| m!"• " ++
-      MessageData.nestD (m!"'{name}'" ++
-        (if name.toString != userName then m!" — \"{userName}\"" else MessageData.nil) ++
-        showDocs docs ++
-        (← showTactics name))
-
-  let tagList : MessageData :=
-    m!"Available tags: {MessageData.nestD (Format.line ++ .joinSep tagDescrs Format.line)}"
-
-  logInfo tagList
-
-/--
-The information needed to display all documentation for a tactic.
--/
-structure TacticDoc where
-  /-- The name of the canonical parser for the tactic -/
-  internalName : Name
-  /-- The user-facing name to display (typically the first keyword token) -/
-  userName : String
-  /-- The tags that have been applied to the tactic -/
-  tags : NameSet
-  /-- The docstring for the tactic -/
-  docString : Option String
-  /-- Any docstring extensions that have been specified -/
-  extensionDocs : Array String
-
-def allTacticDocs : MetaM (Array TacticDoc) := do
-  let env ← getEnv
-  let all :=
-    tacticTagExt.toEnvExtension.getState (← getEnv)
-      |>.importedEntries |>.push (tacticTagExt.exportEntriesFn (tacticTagExt.getState (← getEnv)))
-  let mut tacTags : NameMap NameSet := {}
-  for arr in all do
-    for (tac, tag) in arr do
-      tacTags := tacTags.insert tac (tacTags.findD tac {} |>.insert tag)
-
-  let mut docs := #[]
-
-  let some tactics := (Lean.Parser.parserExtension.getState env).categories.find? `tactic
-    | return #[]
-  for (tac, _) in tactics.kinds do
-    -- Skip noncanonical tactics
-    if let some _ := alternativeOfTactic env tac then continue
-    let userName : String ←
-      if let some descr := env.find? tac |>.bind (·.value?) then
-        if let some tk ← getFirstTk descr then
-          pure tk.trim
-        else pure tac.toString
-      else pure tac.toString
-
-    docs := docs.push {
-      internalName := tac,
-      userName := userName,
-      tags := tacTags.findD tac {},
-      docString := ← findDocString? env tac,
-      extensionDocs := getTacticExtensions env tac
-    }
-  return docs

src/Lean/Elab/Tactic/ElabTerm.lean

@@ -22,15 +22,12 @@ Runs a term elaborator inside a tactic.
 This function ensures that term elaboration fails when backtracking,
 i.e., in `first| tac term | other`.
 -/
-def runTermElab (k : TermElabM α) (mayPostpone := false) : TacticM α :=
-  -- We disable incrementality here so that nested tactics do not unexpectedly use and affect the
-  -- incrementality state of a calling incrementality-enabled tactic.
-  Term.withoutTacticIncrementality true do
-    /- If error recovery is disabled, we disable `Term.withoutErrToSorry` -/
-    if (← read).recover then
-      go
-    else
-      Term.withoutErrToSorry go
+def runTermElab (k : TermElabM α) (mayPostpone := false) : TacticM α := do
+  /- If error recovery is disabled, we disable `Term.withoutErrToSorry` -/
+  if (← read).recover then
+    go
+  else
+    Term.withoutErrToSorry go
 where
   go := k <* Term.synthesizeSyntheticMVars (postpone := .ofBool mayPostpone)
 

src/Lean/Elab/Tactic/Simp.lean

@@ -341,7 +341,7 @@ def mkSimpOnly (stx : Syntax) (usedSimps : Simp.UsedSimps) : MetaM Syntax := do
   let mut localsOrStar := some #[]
   let lctx ← getLCtx
   let env ← getEnv
-  for thm in usedSimps.toArray do
+  for (thm, _) in usedSimps.toArray.qsort (·.2 < ·.2) do
     match thm with
     | .decl declName post inv => -- global definitions in the environment
       if env.contains declName

src/Lean/Elab/Term.lean

@@ -353,7 +353,7 @@ part. `act` is then run on the inner part but with reuse information adjusted as
 For any tactic that participates in reuse, `withNarrowedTacticReuse` should be applied to the
 tactic's syntax and `act` should be used to do recursive tactic evaluation of nested parts.
 -/
-def withNarrowedTacticReuse [Monad m] [MonadWithReaderOf Context m]
+def withNarrowedTacticReuse [Monad m] [MonadExceptOf Exception m] [MonadWithReaderOf Context m]
     [MonadOptions m] [MonadRef m] (split : Syntax → Syntax × Syntax) (act : Syntax → m α)
     (stx : Syntax) : m α := do
   let (outer, inner) := split stx
@@ -377,7 +377,7 @@ NOTE: child nodes after `argIdx` are not tested (which would almost always disab
 necessarily shifted by changes at `argIdx`) so it must be ensured that the result of `arg` does not
 depend on them (i.e. they should not be inspected beforehand).
 -/
-def withNarrowedArgTacticReuse [Monad m] [MonadWithReaderOf Context m]
+def withNarrowedArgTacticReuse [Monad m] [MonadExceptOf Exception m] [MonadWithReaderOf Context m]
     [MonadOptions m] [MonadRef m] (argIdx : Nat) (act : Syntax → m α) (stx : Syntax) : m α :=
   withNarrowedTacticReuse (fun stx => (mkNullNode stx.getArgs[:argIdx], stx[argIdx])) act stx
 
@@ -387,7 +387,7 @@ to `none`. This should be done for tactic blocks that are run multiple times as
 reported progress will jump back and forth (and partial reuse for these kinds of tact blocks is
 similarly questionable).
 -/
-def withoutTacticIncrementality [Monad m] [MonadWithReaderOf Context m] [MonadOptions m]
+def withoutTacticIncrementality [Monad m] [MonadWithReaderOf Context m] [MonadOptions m] [MonadRef m]
     (cond : Bool) (act : m α) : m α := do
   let opts ← getOptions
   withTheReader Term.Context (fun ctx => { ctx with tacSnap? := ctx.tacSnap?.filter fun tacSnap => Id.run do
@@ -398,7 +398,7 @@ def withoutTacticIncrementality [Monad m] [MonadWithReaderOf Context m] [MonadOp
   }) act
 
 /-- Disables incremental tactic reuse for `act` if `cond` is true. -/
-def withoutTacticReuse [Monad m] [MonadWithReaderOf Context m] [MonadOptions m]
+def withoutTacticReuse [Monad m] [MonadWithReaderOf Context m] [MonadOptions m] [MonadRef m]
     (cond : Bool) (act : m α) : m α := do
   let opts ← getOptions
   withTheReader Term.Context (fun ctx => { ctx with tacSnap? := ctx.tacSnap?.map fun tacSnap =>
@@ -1259,8 +1259,8 @@ private def isNoImplicitLambda (stx : Syntax) : Bool :=
 
 private def isTypeAscription (stx : Syntax) : Bool :=
   match stx with
-  | `(($_ : $[$_]?)) => true
-  | _                => false
+  | `(($_ : $_)) => true
+  | _            => false
 
 def hasNoImplicitLambdaAnnotation (type : Expr) : Bool :=
   annotation? `noImplicitLambda type |>.isSome
@@ -1398,7 +1398,7 @@ def resolveLocalName (n : Name) : TermElabM (Option (Expr × List String)) := do
   ```
   def foo.aux := 1
   def foo : Nat → Nat
-    | n => foo.aux -- should not be interpreted as `(foo).aux`
+    | n => foo.aux -- should not be interpreted as `(foo).bar`
   ```
   See test `aStructPerfIssue.lean` for another example.
   We skip auxiliary declarations when `projs` is not empty and `globalDeclFound` is true.
@@ -1415,29 +1415,16 @@ def resolveLocalName (n : Name) : TermElabM (Option (Expr × List String)) := do
   -/
   let rec loop (n : Name) (projs : List String) (globalDeclFound : Bool) := do
     let givenNameView := { view with name := n }
-    let mut globalDeclFoundNext := globalDeclFound
+    let mut globalDeclFound := globalDeclFound
     unless globalDeclFound do
       let r ← resolveGlobalName givenNameView.review
       let r := r.filter fun (_, fieldList) => fieldList.isEmpty
       unless r.isEmpty do
-        globalDeclFoundNext := true
-    /-
-    Note that we use `globalDeclFound` instead of `globalDeclFoundNext` in the following test.
-    Reason: a local should shadow a global with the same name.
-    Consider the following example. See issue #3079
-    ```
-    def foo : Nat := 1
-
-    def bar : Nat :=
-      foo.add 1 -- should be 11
-    where
-      foo := 10
-    ```
-    -/
+        globalDeclFound := true
     match findLocalDecl? givenNameView (skipAuxDecl := globalDeclFound && not projs.isEmpty) with
     | some decl => return some (decl.toExpr, projs)
     | none => match n with
-      | .str pre s => loop pre (s::projs) globalDeclFoundNext
+      | .str pre s => loop pre (s::projs) globalDeclFound
       | _ => return none
   loop view.name [] (globalDeclFound := false)
 
@@ -1849,9 +1836,9 @@ def resolveName' (ident : Syntax) (explicitLevels : List Level) (expectedType? :
       return (c, ids.head!, ids.tail!)
   | _ => throwError "identifier expected"
 
-def resolveId? (stx : Syntax) (kind := "term") (withInfo := false) : TermElabM (Option Expr) := withRef stx do
+def resolveId? (stx : Syntax) (kind := "term") (withInfo := false) : TermElabM (Option Expr) :=
   match stx with
-  | .ident _ _ val preresolved =>
+  | .ident _ _ val preresolved => do
     let rs ← try resolveName stx val preresolved [] catch _ => pure []
     let rs := rs.filter fun ⟨_, projs⟩ => projs.isEmpty
     let fs := rs.map fun (f, _) => f

src/Lean/Environment.lean

@@ -244,21 +244,10 @@ inductive KernelException where
 
 namespace Environment
 
-/--
-Type check given declaration and add it to the environment
--/
+/-- Type check given declaration and add it to the environment -/
 @[extern "lean_add_decl"]
 opaque addDeclCore (env : Environment) (maxHeartbeats : USize) (decl : @& Declaration) : Except KernelException Environment
 
-/--
-Add declaration to kernel without type checking it.
-**WARNING** This function is meant for temporarily working around kernel performance issues.
-It compromises soundness because, for example, a buggy tactic may produce an invalid proof,
-and the kernel will not catch it if the new option is set to true.
--/
-@[extern "lean_add_decl_without_checking"]
-opaque addDeclWithoutChecking (env : Environment) (decl : @& Declaration) : Except KernelException Environment
-
 end Environment
 
 namespace ConstantInfo
@@ -434,51 +423,22 @@ structure ImportM.Context where
 
 abbrev ImportM := ReaderT Lean.ImportM.Context IO
 
-/--
-An environment extension with support for storing/retrieving entries from a .olean file.
- - α is the type of the entries that are stored in .olean files.
- - β is the type of values used to update the state.
- - σ is the actual state.
+/-- An environment extension with support for storing/retrieving entries from a .olean file.
+   - α is the type of the entries that are stored in .olean files.
+   - β is the type of values used to update the state.
+   - σ is the actual state.
 
-For most extensions, α and β coincide. `α` and ‵β` do not coincide for extensions where the data
-used to update the state contains elements which cannot be stored in files (for example, closures).
+   Remark: for most extensions α and β coincide.
 
-During elaboration of a module, state of type `σ` can be both read and written. When elaboration is
-complete, the state of type `σ` is converted to serialized state of type `Array α` by
-`exportEntriesFn`. To read the current module's state, use `PersistentEnvExtension.getState`. To
-modify it, use `PersistentEnvExtension.addEntry`, with an `addEntryFn` that performs the appropriate
-modification.
+   Note that `addEntryFn` is not in `IO`. This is intentional, and allows us to write simple functions such as
+   ```
+   def addAlias (env : Environment) (a : Name) (e : Name) : Environment :=
+   aliasExtension.addEntry env (a, e)
+   ```
+   without using `IO`. We have many functions like `addAlias`.
 
-When a module is loaded, the values saved by all of its dependencies for this
-`PersistentEnvExtension` are are available as an `Array (Array α)` via the environment extension,
-with one array per transitively imported module. The state of type `σ` used in the current module
-can be initialized from these imports by specifying a suitable `addImportedFn`. The `addImportedFn`
-runs at the beginning of elaboration for every module, so it's usually better for performance to
-query the array of imported modules directly, because only a fraction of imported entries is usually
-queried during elaboration of a module.
-
-The most typical pattern for using `PersistentEnvExtension` is to set `σ` to a datatype such as
-`NameMap` that efficiently tracks data for the current module. Then, in `exportEntriesFn`, this type
-is converted to an array of pairs, sorted by the key. Given `ext : PersistentEnvExtension α β σ` and
-`env : Environment`, the complete array of imported entries sorted by module index can be obtained
-using `(ext.toEnvExtension.getState env).importedEntries`. To query the extension for some constant
-name `n`, first use `env.getModuleIdxFor? n`. If it returns `none`, look up `n` in the current
-module's state (the `NameMap`). If it returns `some idx`, use `ext.getModuleEntries env idx` to get
-the array of entries for `n`'s defining module, and query it using `Array.binSearch`. This pattern
-imposes a constraint that the extension can only track metadata that is declared in the same module
-as the definition to which it applies; relaxing this restriction can make queries slower due to
-needing to search _all_ modules. If it is necessary to search all modules, it is usually better to
-initialize the state of type `σ` once from all imported entries and choose a more efficient search
-datastructure for it.
-
-Note that `addEntryFn` is not in `IO`. This is intentional, and allows us to write simple functions
-such as
-```
-def addAlias (env : Environment) (a : Name) (e : Name) : Environment :=
-aliasExtension.addEntry env (a, e)
-```
-without using `IO`. We have many functions like `addAlias`.
--/
+   `α` and ‵β` do not coincide for extensions where the data used to update the state contains, for example,
+   closures which we currently cannot store in files. -/
 structure PersistentEnvExtension (α : Type) (β : Type) (σ : Type) where
   toEnvExtension  : EnvExtension (PersistentEnvExtensionState α σ)
   name            : Name
@@ -639,7 +599,7 @@ end TagDeclarationExtension
 
 def MapDeclarationExtension (α : Type) := SimplePersistentEnvExtension (Name × α) (NameMap α)
 
-def mkMapDeclarationExtension (name : Name := by exact decl_name%) : IO (MapDeclarationExtension α) :=
+def mkMapDeclarationExtension [Inhabited α] (name : Name := by exact decl_name%) : IO (MapDeclarationExtension α) :=
   registerSimplePersistentEnvExtension {
     name          := name,
     addImportedFn := fun _ => {},
@@ -1024,6 +984,9 @@ def displayStats (env : Environment) : IO Unit := do
   IO.println ("direct imports:                        " ++ toString env.header.imports);
   IO.println ("number of imported modules:            " ++ toString env.header.regions.size);
   IO.println ("number of memory-mapped modules:       " ++ toString (env.header.regions.filter (·.isMemoryMapped) |>.size));
+  IO.println ("number of consts:                      " ++ toString env.constants.size);
+  IO.println ("number of imported consts:             " ++ toString env.constants.stageSizes.1);
+  IO.println ("number of local consts:                " ++ toString env.constants.stageSizes.2);
   IO.println ("number of buckets for imported consts: " ++ toString env.constants.numBuckets);
   IO.println ("trust level:                           " ++ toString env.header.trustLevel);
   IO.println ("number of extensions:                  " ++ toString env.extensions.size);
@@ -1100,11 +1063,4 @@ instance (m n) [MonadLift m n] [MonadEnv m] : MonadEnv n where
   getEnv    := liftM (getEnv : m Environment)
   modifyEnv := fun f => liftM (modifyEnv f : m Unit)
 
-/-- Constructs a DefinitionVal, inferring the `unsafe` field -/
-def mkDefinitionValInferrringUnsafe [Monad m] [MonadEnv m] (name : Name) (levelParams : List Name)
-    (type : Expr) (value : Expr) (hints : ReducibilityHints) : m DefinitionVal := do
-  let env ← getEnv
-  let safety := if env.hasUnsafe type || env.hasUnsafe value then DefinitionSafety.unsafe else DefinitionSafety.safe
-  return { name, levelParams, type, value, hints, safety }
-
 end Lean

src/Lean/HeadIndex.lean

@@ -32,6 +32,8 @@ inductive HeadIndex where
   | forallE
   deriving Inhabited, BEq, Repr
 
+namespace HeadIndex
+
 /-- Hash code for a `HeadIndex` value. -/
 protected def HeadIndex.hash : HeadIndex → UInt64
   | fvar fvarId         => mixHash 11 <| hash fvarId
@@ -45,6 +47,8 @@ protected def HeadIndex.hash : HeadIndex → UInt64
 
 instance : Hashable HeadIndex := ⟨HeadIndex.hash⟩
 
+end HeadIndex
+
 namespace Expr
 
 /-- Return the number of arguments in the given expression with respect to its `HeadIndex` -/

src/Lean/Meta/AbstractMVars.lean

@@ -7,6 +7,13 @@ prelude
 import Lean.Meta.Basic
 
 namespace Lean.Meta
+
+structure AbstractMVarsResult where
+  paramNames : Array Name
+  numMVars   : Nat
+  expr       : Expr
+  deriving Inhabited, BEq
+
 namespace AbstractMVars
 
 structure State where

src/Lean/Meta/Basic.lean

@@ -222,14 +222,7 @@ structure SynthInstanceCacheKey where
   synthPendingDepth : Nat
   deriving Hashable, BEq
 
-/-- Resulting type for `abstractMVars` -/
-structure AbstractMVarsResult where
-  paramNames : Array Name
-  numMVars   : Nat
-  expr       : Expr
-  deriving Inhabited, BEq
-
-abbrev SynthInstanceCache := PersistentHashMap SynthInstanceCacheKey (Option AbstractMVarsResult)
+abbrev SynthInstanceCache := PersistentHashMap SynthInstanceCacheKey (Option Expr)
 
 abbrev InferTypeCache := PersistentExprStructMap Expr
 abbrev FunInfoCache   := PersistentHashMap InfoCacheKey FunInfo
@@ -919,8 +912,8 @@ def mkForallFVars (xs : Array Expr) (e : Expr) (usedOnly : Bool := false) (usedL
 /-- Takes an array `xs` of free variables and metavariables and a
 body term `e` and creates `fun ..xs => e`, suitably
 abstracting `e` and the types in `xs`. -/
-def mkLambdaFVars (xs : Array Expr) (e : Expr) (usedOnly : Bool := false) (usedLetOnly : Bool := true) (etaReduce : Bool := false) (binderInfoForMVars := BinderInfo.implicit) : MetaM Expr :=
-  if xs.isEmpty then return e else liftMkBindingM <| MetavarContext.mkLambda xs e usedOnly usedLetOnly etaReduce binderInfoForMVars
+def mkLambdaFVars (xs : Array Expr) (e : Expr) (usedOnly : Bool := false) (usedLetOnly : Bool := true) (binderInfoForMVars := BinderInfo.implicit) : MetaM Expr :=
+  if xs.isEmpty then return e else liftMkBindingM <| MetavarContext.mkLambda xs e usedOnly usedLetOnly binderInfoForMVars
 
 def mkLetFVars (xs : Array Expr) (e : Expr) (usedLetOnly := true) (binderInfoForMVars := BinderInfo.implicit) : MetaM Expr :=
   mkLambdaFVars xs e (usedLetOnly := usedLetOnly) (binderInfoForMVars := binderInfoForMVars)

src/Lean/Meta/Closure.lean

@@ -349,9 +349,14 @@ end Closure
 def mkAuxDefinition (name : Name) (type : Expr) (value : Expr) (zetaDelta : Bool := false) (compile : Bool := true) : MetaM Expr := do
   let result ← Closure.mkValueTypeClosure type value zetaDelta
   let env ← getEnv
-  let hints := ReducibilityHints.regular (getMaxHeight env result.value + 1)
-  let decl := Declaration.defnDecl (← mkDefinitionValInferrringUnsafe name result.levelParams.toList
-    result.type result.value  hints)
+  let decl := Declaration.defnDecl {
+    name        := name
+    levelParams := result.levelParams.toList
+    type        := result.type
+    value       := result.value
+    hints       := ReducibilityHints.regular (getMaxHeight env result.value + 1)
+    safety      := if env.hasUnsafe result.type || env.hasUnsafe result.value then DefinitionSafety.unsafe else DefinitionSafety.safe
+  }
   addDecl decl
   if compile then
     compileDecl decl

src/Lean/Meta/CompletionName.lean

@@ -25,6 +25,7 @@ namespace Lean.Meta
 
 builtin_initialize completionBlackListExt : TagDeclarationExtension ← mkTagDeclarationExtension
 
+@[export lean_completion_add_to_black_list]
 def addToCompletionBlackList (env : Environment) (declName : Name) : Environment :=
   completionBlackListExt.tag env declName
 

src/Lean/Meta/Constructions.lean

@@ -7,46 +7,33 @@ prelude
 import Lean.AuxRecursor
 import Lean.AddDecl
 import Lean.Meta.AppBuilder
-import Lean.Meta.CompletionName
-import Lean.Meta.Constructions.RecOn
-import Lean.Meta.Constructions.BRecOn
 
 namespace Lean
 
-@[extern "lean_mk_cases_on"] opaque mkCasesOnImp (env : Environment) (declName : @& Name) : Except KernelException Declaration
-@[extern "lean_mk_no_confusion_type"] opaque mkNoConfusionTypeCoreImp (env : Environment) (declName : @& Name) : Except KernelException Declaration
-@[extern "lean_mk_no_confusion"] opaque mkNoConfusionCoreImp (env : Environment) (declName : @& Name) : Except KernelException Declaration
+@[extern "lean_mk_cases_on"] opaque mkCasesOnImp (env : Environment) (declName : @& Name) : Except KernelException Environment
+@[extern "lean_mk_rec_on"] opaque mkRecOnImp (env : Environment) (declName : @& Name) : Except KernelException Environment
+@[extern "lean_mk_no_confusion"] opaque mkNoConfusionCoreImp (env : Environment) (declName : @& Name) : Except KernelException Environment
+@[extern "lean_mk_below"] opaque mkBelowImp (env : Environment) (declName : @& Name) : Except KernelException Environment
+@[extern "lean_mk_ibelow"] opaque mkIBelowImp (env : Environment) (declName : @& Name) : Except KernelException Environment
+@[extern "lean_mk_brec_on"] opaque mkBRecOnImp (env : Environment) (declName : @& Name) : Except KernelException Environment
+@[extern "lean_mk_binduction_on"] opaque mkBInductionOnImp (env : Environment) (declName : @& Name) : Except KernelException Environment
+
+variable [Monad m] [MonadEnv m] [MonadError m] [MonadOptions m]
+
+@[inline] private def adaptFn (f : Environment → Name → Except KernelException Environment) (declName : Name) : m Unit := do
+  let env ← ofExceptKernelException (f (← getEnv) declName)
+  modifyEnv fun _ => env
+
+def mkCasesOn (declName : Name) : m Unit := adaptFn mkCasesOnImp declName
+def mkRecOn (declName : Name) : m Unit := adaptFn mkRecOnImp declName
+def mkNoConfusionCore (declName : Name) : m Unit := adaptFn mkNoConfusionCoreImp declName
+def mkBelow (declName : Name) : m Unit := adaptFn mkBelowImp declName
+def mkIBelow (declName : Name) : m Unit := adaptFn mkIBelowImp declName
+def mkBRecOn (declName : Name) : m Unit := adaptFn mkBRecOnImp declName
+def mkBInductionOn (declName : Name) : m Unit := adaptFn mkBInductionOnImp declName
 
 open Meta
 
-def mkCasesOn (declName : Name) : MetaM Unit := do
-  let name := mkCasesOnName declName
-  let decl ← ofExceptKernelException (mkCasesOnImp (← getEnv) declName)
-  addDecl decl
-  setReducibleAttribute name
-  modifyEnv fun env => markAuxRecursor env name
-  modifyEnv fun env => addProtected env name
-
-def mkNoConfusionCore (declName : Name) : MetaM Unit := do
-  -- Do not do anything unless can_elim_to_type. TODO: Extract to util
-  let .inductInfo indVal ← getConstInfo declName | return
-  let recInfo ← getConstInfo (mkRecName declName)
-  unless recInfo.levelParams.length > indVal.levelParams.length do return
-
-  let name := Name.mkStr declName "noConfusionType"
-  let decl ← ofExceptKernelException (mkNoConfusionTypeCoreImp (← getEnv) declName)
-  addDecl decl
-  setReducibleAttribute name
-  modifyEnv fun env => addToCompletionBlackList env name
-  modifyEnv fun env => addProtected env name
-
-  let name := Name.mkStr declName "noConfusion"
-  let decl ← ofExceptKernelException (mkNoConfusionCoreImp (← getEnv) declName)
-  addDecl decl
-  setReducibleAttribute name
-  modifyEnv fun env => markNoConfusion env name
-  modifyEnv fun env => addProtected env name
-
 def mkNoConfusionEnum (enumName : Name) : MetaM Unit := do
   if (← getEnv).contains ``noConfusionEnum then
     mkToCtorIdx
@@ -56,6 +43,7 @@ def mkNoConfusionEnum (enumName : Name) : MetaM Unit := do
     -- `noConfusionEnum` was not defined yet, so we use `mkNoConfusionCore`
     mkNoConfusionCore enumName
 where
+
   mkToCtorIdx : MetaM Unit := do
     let ConstantInfo.inductInfo info ← getConstInfo enumName | unreachable!
     let us := info.levelParams.map mkLevelParam

src/Lean/Meta/Constructions/BRecOn.lean

@@ -1,393 +0,0 @@
-/-
-Copyright (c) 2024 Lean FRO. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura, Joachim Breitner
--/
-prelude
-import Lean.Meta.InferType
-import Lean.AuxRecursor
-import Lean.AddDecl
-import Lean.Meta.CompletionName
-
-namespace Lean
-open Meta
-
-section PProd
-
-/--!
-Helpers to construct types and values of `PProd` and project out of them, set up to use `And`
-instead of `PProd` if the universes allow. Maybe be extracted into a Utils module when useful
-elsewhere.
--/
-
-private def mkPUnit : Level → Expr
-  | .zero => .const ``True []
-  | lvl   => .const ``PUnit [lvl]
-
-private def mkPProd (e1 e2 : Expr) : MetaM Expr := do
-  let lvl1 ← getLevel e1
-  let lvl2 ← getLevel e2
-  if lvl1 matches .zero && lvl2 matches .zero then
-    return mkApp2 (.const `And []) e1 e2
-  else
-    return mkApp2 (.const ``PProd [lvl1, lvl2]) e1 e2
-
-private def mkNProd (lvl : Level) (es : Array Expr) : MetaM Expr :=
-  es.foldrM (init := mkPUnit lvl) mkPProd
-
-private def mkPUnitMk : Level → Expr
-  | .zero => .const ``True.intro []
-  | lvl   => .const ``PUnit.unit [lvl]
-
-private def mkPProdMk (e1 e2 : Expr) : MetaM Expr := do
-  let t1 ← inferType e1
-  let t2 ← inferType e2
-  let lvl1 ← getLevel t1
-  let lvl2 ← getLevel t2
-  if lvl1 matches .zero && lvl2 matches .zero then
-    return mkApp4 (.const ``And.intro []) t1 t2 e1 e2
-  else
-    return mkApp4 (.const ``PProd.mk [lvl1, lvl2]) t1 t2 e1 e2
-
-private def mkNProdMk (lvl : Level) (es : Array Expr) : MetaM Expr :=
-  es.foldrM (init := mkPUnitMk lvl) mkPProdMk
-
-/-- `PProd.fst` or `And.left` (as projections) -/
-private def mkPProdFst (e : Expr) : MetaM Expr := do
-  let t ← whnf (← inferType e)
-  match_expr t with
-  | PProd _ _ => return .proj ``PProd 0 e
-  | And _ _ =>   return .proj ``And 0 e
-  | _ => throwError "Cannot project .1 out of{indentExpr e}\nof type{indentExpr t}"
-
-/-- `PProd.snd` or `And.right` (as projections) -/
-private def mkPProdSnd (e : Expr) : MetaM Expr := do
-  let t ← whnf (← inferType e)
-  match_expr t with
-  | PProd _ _ => return .proj ``PProd 1 e
-  | And _ _ =>   return .proj ``And 1 e
-  | _ => throwError "Cannot project .2 out of{indentExpr e}\nof type{indentExpr t}"
-
-end PProd
-
-/--
-If `minorType` is the type of a minor premies of a recursor, such as
-```
-  (cons : (head : α) → (tail : List α) → (tail_hs : motive tail) → motive (head :: tail))
-```
-of `List.rec`, constructs the corresponding argument to `List.rec` in the construction
-of `.below` definition; in this case
-```
-fun head tail tail_ih =>
-  PProd (PProd (motive tail) tail_ih) PUnit
-```
-of type
-```
-α → List α → Sort (max 1 u_1) → Sort (max 1 u_1)
-```
-The parameter `typeFormers` are the `motive`s.
--/
-private def buildBelowMinorPremise (rlvl : Level) (typeFormers : Array Expr) (minorType : Expr) : MetaM Expr :=
-  forallTelescope minorType fun minor_args _ => do go #[] minor_args.toList
-where
-  ibelow := rlvl matches .zero
-  go (prods : Array Expr) : List Expr → MetaM Expr
-  | [] => mkNProd rlvl prods
-  | arg::args => do
-    let argType ← inferType arg
-    forallTelescope argType fun arg_args arg_type => do
-      if typeFormers.contains arg_type.getAppFn then
-        let name ← arg.fvarId!.getUserName
-        let type' ← forallTelescope argType fun args _ => mkForallFVars args (.sort rlvl)
-        withLocalDeclD name type' fun arg' => do
-          let snd ← mkForallFVars arg_args (mkAppN arg' arg_args)
-          let e' ← mkPProd argType snd
-          mkLambdaFVars #[arg'] (← go (prods.push e') args)
-      else
-        mkLambdaFVars #[arg] (← go prods args)
-
-/--
-Constructs the `.below` or `.ibelow` definition for a inductive predicate.
-
-For example for the `List` type, it constructs,
-```
-@[reducible] protected def List.below.{u_1, u} : {α : Type u} →
-  {motive : List α → Sort u_1} → List α → Sort (max 1 u_1) :=
-fun {α} {motive} t =>
-  List.rec PUnit (fun head tail tail_ih => PProd (PProd (motive tail) tail_ih) PUnit) t
-```
-and
-```
-@[reducible] protected def List.ibelow.{u} : {α : Type u} →
-  {motive : List α → Prop} → List α → Prop :=
-fun {α} {motive} t =>
-  List.rec True (fun head tail tail_ih => (motive tail ∧ tail_ih) ∧ True) t
-```
--/
-private def mkBelowOrIBelow (indName : Name) (ibelow : Bool) : MetaM Unit := do
-  let .inductInfo indVal ← getConstInfo indName | return
-  unless indVal.isRec do return
-  if ← isPropFormerType indVal.type then return
-
-  let recName := mkRecName indName
-  -- The construction follows the type of `ind.rec`
-  let .recInfo recVal ← getConstInfo recName
-    | throwError "{recName} not a .recInfo"
-  let lvl::lvls := recVal.levelParams.map (Level.param ·)
-    | throwError "recursor {recName} has no levelParams"
-  let lvlParam := recVal.levelParams.head!
-  -- universe parameter names of ibelow/below
-  let blvls :=
-    -- For ibelow we instantiate the first universe parameter of `.rec` to `.zero`
-    if ibelow then recVal.levelParams.tail!
-              else recVal.levelParams
-  let .some ilvl ← typeFormerTypeLevel indVal.type
-    | throwError "type {indVal.type} of inductive {indVal.name} not a type former?"
-
-  -- universe level of the resultant type
-  let rlvl : Level :=
-    if ibelow then
-      0
-    else if indVal.isReflexive then
-      if let .max 1 lvl := ilvl then
-        mkLevelMax' (.succ lvl) lvl
-      else
-        mkLevelMax' (.succ lvl) ilvl
-    else
-      mkLevelMax' 1 lvl
-
-  let refType :=
-    if ibelow then
-      recVal.type.instantiateLevelParams [lvlParam] [0]
-    else if indVal.isReflexive then
-      recVal.type.instantiateLevelParams [lvlParam] [lvl.succ]
-    else
-      recVal.type
-
-  let decl ← forallTelescope refType fun refArgs _ => do
-    assert! refArgs.size == indVal.numParams + recVal.numMotives + recVal.numMinors + indVal.numIndices + 1
-    let params      : Array Expr := refArgs[:indVal.numParams]
-    let typeFormers : Array Expr := refArgs[indVal.numParams:indVal.numParams + recVal.numMotives]
-    let minors      : Array Expr := refArgs[indVal.numParams + recVal.numMotives:indVal.numParams + recVal.numMotives + recVal.numMinors]
-    let remaining   : Array Expr := refArgs[indVal.numParams + recVal.numMotives + recVal.numMinors:]
-
-    let mut val := .const recName (rlvl.succ :: lvls)
-    -- add parameters
-    val := mkAppN val params
-    -- add type formers
-    for typeFormer in typeFormers do
-      let arg ← forallTelescope (← inferType typeFormer) fun targs _ =>
-        mkLambdaFVars targs (.sort rlvl)
-      val := .app val arg
-    -- add minor premises
-    for minor in minors do
-      let arg ← buildBelowMinorPremise rlvl typeFormers (← inferType minor)
-      val := .app val arg
-    -- add indices and major premise
-    val := mkAppN val remaining
-
-    -- All paramaters of `.rec` besides the `minors` become parameters of `.below`
-    let below_params := params ++ typeFormers ++ remaining
-    let type ← mkForallFVars below_params (.sort rlvl)
-    val ← mkLambdaFVars below_params val
-
-    let name := if ibelow then mkIBelowName indName else mkBelowName indName
-    mkDefinitionValInferrringUnsafe name blvls type val .abbrev
-
-  addDecl (.defnDecl decl)
-  setReducibleAttribute decl.name
-  modifyEnv fun env => markAuxRecursor env decl.name
-  modifyEnv fun env => addProtected env decl.name
-
-def mkBelow (declName : Name) : MetaM Unit := mkBelowOrIBelow declName true
-def mkIBelow (declName : Name) : MetaM Unit := mkBelowOrIBelow declName false
-
-/--
-If `minorType` is the type of a minor premies of a recursor, such as
-```
-  (cons : (head : α) → (tail : List α) → (tail_hs : motive tail) → motive (head :: tail))
-```
-of `List.rec`, constructs the corresponding argument to `List.rec` in the construction
-of `.brecOn` definition; in this case
-```
-fun head tail tail_ih =>
-  ⟨F_1 (head :: tail) ⟨tail_ih, PUnit.unit⟩, ⟨tail_ih, PUnit.unit⟩⟩
-```
-of type
-```
-(head : α) → (tail : List α) →
-  PProd (motive tail) (List.below tail) →
-  PProd (motive (head :: tail)) (PProd (PProd (motive tail) (List.below tail)) PUnit)
-```
-The parameter `typeFormers` are the `motive`s.
--/
-private def buildBRecOnMinorPremise (rlvl : Level) (typeFormers : Array Expr)
-    (belows : Array Expr) (fs : Array Expr) (minorType : Expr) : MetaM Expr :=
-  forallTelescope minorType fun minor_args minor_type => do
-    let rec go (prods : Array Expr) : List Expr → MetaM Expr
-      | [] => minor_type.withApp fun minor_type_fn minor_type_args => do
-          let b ← mkNProdMk rlvl prods
-          let .some ⟨idx, _⟩ := typeFormers.indexOf? minor_type_fn
-            | throwError m!"Did not find {minor_type} in {typeFormers}"
-          mkPProdMk (mkAppN fs[idx]! (minor_type_args.push b)) b
-      | arg::args => do
-        let argType ← inferType arg
-        forallTelescope argType fun arg_args arg_type => do
-          arg_type.withApp fun arg_type_fn arg_type_args => do
-            if let .some idx := typeFormers.indexOf? arg_type_fn then
-              let name ← arg.fvarId!.getUserName
-              let type' ← mkForallFVars arg_args
-                (← mkPProd arg_type (mkAppN belows[idx]! arg_type_args) )
-              withLocalDeclD name type' fun arg' => do
-                if arg_args.isEmpty then
-                  mkLambdaFVars #[arg'] (← go (prods.push arg') args)
-                else
-                  let r := mkAppN arg' arg_args
-                  let r₁ ← mkLambdaFVars arg_args (← mkPProdFst r)
-                  let r₂ ← mkLambdaFVars arg_args (← mkPProdSnd r)
-                  let r ← mkPProdMk r₁ r₂
-                  mkLambdaFVars #[arg'] (← go (prods.push r) args)
-            else
-              mkLambdaFVars #[arg] (← go prods args)
-    go #[] minor_args.toList
-
-/--
-Constructs the `.brecon` or `.binductionon` definition for a inductive predicate.
-
-For example for the `List` type, it constructs,
-```
-@[reducible] protected def List.brecOn.{u_1, u} : {α : Type u} → {motive : List α → Sort u_1} →
-  (t : List α) → ((t : List α) → List.below t → motive t) → motive t :=
-fun {α} {motive} t (F_1 : (t : List α) → List.below t → motive t) => (
-  @List.rec α (fun t => PProd (motive t) (@List.below α motive t))
-    ⟨F_1 [] PUnit.unit, PUnit.unit⟩
-    (fun head tail tail_ih => ⟨F_1 (head :: tail) ⟨tail_ih, PUnit.unit⟩, ⟨tail_ih, PUnit.unit⟩⟩)
-    t
-  ).1
-```
-and
-```
-@[reducible] protected def List.binductionOn.{u} : ∀ {α : Type u} {motive : List α → Prop}
-  (t : List α), (∀ (t : List α), List.ibelow t → motive t) → motive t :=
-fun {α} {motive} t F_1 => (
-  @List.rec α (fun t => And (motive t) (@List.ibelow α motive t))
-    ⟨F_1 [] True.intro, True.intro⟩
-    (fun head tail tail_ih => ⟨F_1 (head :: tail) ⟨tail_ih, True.intro⟩, ⟨tail_ih, True.intro⟩⟩)
-    t
-  ).1
-```
--/
-def mkBRecOnOrBInductionOn (indName : Name) (ind : Bool) : MetaM Unit := do
-  let .inductInfo indVal ← getConstInfo indName | return
-  unless indVal.isRec do return
-  if ← isPropFormerType indVal.type then return
-  let recName := mkRecName indName
-  let .recInfo recVal ← getConstInfo recName | return
-  unless recVal.numMotives = indVal.all.length do
-    /-
-    The mutual declaration containing `declName` contains nested inductive datatypes.
-    We don't support this kind of declaration here yet. We probably never will :)
-    To support it, we will need to generate an auxiliary `below` for each nested inductive
-    type since their default `below` is not good here. For example, at
-    ```
-    inductive Term
-    | var : String -> Term
-    | app : String -> List Term -> Term
-    ```
-    The `List.below` is not useful since it will not allow us to recurse over the nested terms.
-    We need to generate another one using the auxiliary recursor `Term.rec_1` for `List Term`.
-    -/
-    return
-
-  let lvl::lvls := recVal.levelParams.map (Level.param ·)
-    | throwError "recursor {recName} has no levelParams"
-  let lvlParam := recVal.levelParams.head!
-  -- universe parameter names of brecOn/binductionOn
-  let blps := if ind then recVal.levelParams.tail!  else recVal.levelParams
-  -- universe arguments of below/ibelow
-  let blvls := if ind then lvls else lvl::lvls
-
-  let .some ⟨idx, _⟩ := indVal.all.toArray.indexOf? indName
-    | throwError m!"Did not find {indName} in {indVal.all}"
-
-  let .some ilvl ← typeFormerTypeLevel indVal.type
-    | throwError "type {indVal.type} of inductive {indVal.name} not a type former?"
-  -- universe level of the resultant type
-  let rlvl : Level :=
-    if ind then
-      0
-    else if indVal.isReflexive then
-      if let .max 1 lvl := ilvl then
-        mkLevelMax' (.succ lvl) lvl
-      else
-        mkLevelMax' (.succ lvl) ilvl
-    else
-      mkLevelMax' 1 lvl
-
-  let refType :=
-    if ind then
-      recVal.type.instantiateLevelParams [lvlParam] [0]
-    else if indVal.isReflexive then
-      recVal.type.instantiateLevelParams [lvlParam] [lvl.succ]
-    else
-      recVal.type
-
-  let decl ← forallTelescope refType fun refArgs _ => do
-    assert! refArgs.size == indVal.numParams + recVal.numMotives + recVal.numMinors + indVal.numIndices + 1
-    let params      : Array Expr := refArgs[:indVal.numParams]
-    let typeFormers : Array Expr := refArgs[indVal.numParams:indVal.numParams + recVal.numMotives]
-    let minors      : Array Expr := refArgs[indVal.numParams + recVal.numMotives:indVal.numParams + recVal.numMotives + recVal.numMinors]
-    let remaining   : Array Expr := refArgs[indVal.numParams + recVal.numMotives + recVal.numMinors:]
-
-    -- One `below` for each type former (same parameters)
-    let belows := indVal.all.toArray.map fun n =>
-      let belowName := if ind then mkIBelowName n else mkBelowName n
-      mkAppN (.const belowName blvls) (params ++ typeFormers)
-
-    -- create types of functionals (one for each type former)
-    --   (F_1 : (t : List α) → (f : List.below t) → motive t)
-    -- and bring parameters of that type into scope
-    let mut fDecls : Array (Name × (Array Expr -> MetaM Expr)) := #[]
-    for typeFormer in typeFormers, below in belows, i in [:typeFormers.size] do
-      let fType ← forallTelescope (← inferType typeFormer) fun targs _ => do
-        withLocalDeclD `f (mkAppN below targs) fun f =>
-          mkForallFVars (targs.push f) (mkAppN typeFormer targs)
-      let fName := .mkSimple s!"F_{i + 1}"
-      fDecls := fDecls.push (fName, fun _ => pure fType)
-    withLocalDeclsD fDecls fun fs => do
-      let mut val := .const recName (rlvl :: lvls)
-      -- add parameters
-      val := mkAppN val params
-      -- add type formers
-      for typeFormer in typeFormers, below in belows do
-        -- example: (motive := fun t => PProd (motive t) (@List.below α motive t))
-        let arg ← forallTelescope (← inferType typeFormer) fun targs _ => do
-          let cType := mkAppN typeFormer targs
-          let belowType := mkAppN below targs
-          let arg ← mkPProd cType belowType
-          mkLambdaFVars targs arg
-        val := .app val arg
-      -- add minor premises
-      for minor in minors do
-        let arg ← buildBRecOnMinorPremise rlvl typeFormers belows fs (← inferType minor)
-        val := .app val arg
-      -- add indices and major premise
-      val := mkAppN val remaining
-      -- project out first component
-      val ← mkPProdFst val
-
-      -- All paramaters of `.rec` besides the `minors` become parameters of `.bRecOn`, and the `fs`
-      let below_params := params ++ typeFormers ++ remaining ++ fs
-      let type ← mkForallFVars below_params (mkAppN typeFormers[idx]! remaining)
-      val ← mkLambdaFVars below_params val
-
-      let name := if ind then mkBInductionOnName indName else mkBRecOnName indName
-      mkDefinitionValInferrringUnsafe name blps type val .abbrev
-
-  addDecl (.defnDecl decl)
-  setReducibleAttribute decl.name
-  modifyEnv fun env => markAuxRecursor env decl.name
-  modifyEnv fun env => addProtected env decl.name
-
-def mkBRecOn (declName : Name) : MetaM Unit := mkBRecOnOrBInductionOn declName false
-def mkBInductionOn (declName : Name) : MetaM Unit := mkBRecOnOrBInductionOn declName true

src/Lean/Meta/Constructions/RecOn.lean

@@ -1,35 +0,0 @@
-/-
-Copyright (c) 2024 Lean FRO. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura, Joachim Breitner
--/
-prelude
-import Lean.Meta.InferType
-import Lean.AuxRecursor
-import Lean.AddDecl
-import Lean.Meta.CompletionName
-
-open Lean Meta
-
-def mkRecOn (n : Name) : MetaM Unit := do
-  let .recInfo recInfo ← getConstInfo (mkRecName n)
-    | throwError "{mkRecName n} not a recinfo"
-  let decl ← forallTelescope recInfo.type fun xs t => do
-    let e := .const recInfo.name (recInfo.levelParams.map (.param ·))
-    let e := mkAppN e xs
-    -- We reorder the parameters
-    -- before: As Cs minor_premises indices major-premise
-    -- fow:    As Cs indices major-premise minor-premises
-    let AC_size := xs.size - recInfo.numMinors - recInfo.numIndices - 1
-    let vs :=
-      xs[:AC_size] ++
-      xs[AC_size + recInfo.numMinors:AC_size + recInfo.numMinors + 1 + recInfo.numIndices] ++
-      xs[AC_size:AC_size + recInfo.numMinors]
-    let type ← mkForallFVars vs t
-    let value ← mkLambdaFVars vs e
-    mkDefinitionValInferrringUnsafe (mkRecOnName n) recInfo.levelParams type value .abbrev
-
-  addDecl (.defnDecl decl)
-  setReducibleAttribute decl.name
-  modifyEnv fun env => markAuxRecursor env decl.name
-  modifyEnv fun env => addProtected env decl.name

src/Lean/Meta/DiscrTree.lean

@@ -850,7 +850,7 @@ def foldValues (f : σ → α → σ) (init : σ) (t : DiscrTree α) : σ :=
 Check for the presence of a value satisfying a predicate.
 -/
 @[inline]
-def containsValueP (t : DiscrTree α) (f : α → Bool) : Bool :=
+def containsValueP [BEq α] (t : DiscrTree α) (f : α → Bool) : Bool :=
   t.foldValues (init := false) fun r a => r || f a
 
 /--

src/Lean/Meta/ExprDefEq.lean

@@ -419,10 +419,10 @@ where the index is the position in the local context.
 -/
 private partial def mkLambdaFVarsWithLetDeps (xs : Array Expr) (v : Expr) : MetaM (Option Expr) := do
   if not (← hasLetDeclsInBetween) then
-    mkLambdaFVars xs v (etaReduce := true)
+    mkLambdaFVars xs v
   else
     let ys ← addLetDeps
-    mkLambdaFVars ys v (etaReduce := true)
+    mkLambdaFVars ys v
 
 where
   /-- Return true if there are let-declarions between `xs[0]` and `xs[xs.size-1]`.
@@ -1775,12 +1775,15 @@ private partial def isDefEqQuickOther (t s : Expr) : MetaM LBool := do
         | LBool.true => return LBool.true
         | LBool.false => return LBool.false
         | _ =>
-          let ctx ← read
-          if ctx.config.isDefEqStuckEx then do
-            trace[Meta.isDefEq.stuck] "{t} =?= {s}"
-            Meta.throwIsDefEqStuck
+          if tFn.isMVar || sFn.isMVar then
+            let ctx ← read
+            if ctx.config.isDefEqStuckEx then do
+              trace[Meta.isDefEq.stuck] "{t} =?= {s}"
+              Meta.throwIsDefEqStuck
+            else
+              return LBool.false
           else
-            return LBool.false
+            return LBool.undef
       else
         isDefEqQuickMVarMVar t s
 

src/Lean/Meta/IndPredBelow.lean

@@ -434,7 +434,7 @@ partial def mkBelowMatcher
   withExistingLocalDecls (lhss.foldl (init := []) fun s v => s ++ v.fvarDecls) do
     for lhs in lhss do
       trace[Meta.IndPredBelow.match] "{lhs.patterns.map (·.toMessageData)}"
-  let res ← Match.mkMatcher (exceptionIfContainsSorry := true) { matcherName, matchType, discrInfos := mkArray (mkMatcherInput.numDiscrs + 1) {}, lhss }
+  let res ← Match.mkMatcher { matcherName, matchType, discrInfos := mkArray (mkMatcherInput.numDiscrs + 1) {}, lhss }
   res.addMatcher
   -- if a wrong index is picked, the resulting matcher can be type-incorrect.
   -- we check here, so that errors can propagate higher up the call stack.

src/Lean/Meta/InferType.lean

@@ -377,41 +377,29 @@ def isType (e : Expr) : MetaM Bool := do
   withReader (fun ctx => { ctx with lctx := ctx.lctx.mkLocalDecl fvarId name type bi }) do
     x (mkFVar fvarId)
 
-def typeFormerTypeLevelQuick : Expr → Option Level
-  | .forallE _ _ b _ => typeFormerTypeLevelQuick b
-  | .sort l => some l
-  | _ => none
-
-/--
-Return `u` iff `type` is `Sort u` or `As → Sort u`.
--/
-partial def typeFormerTypeLevel (type : Expr) : MetaM (Option Level) := do
-  match typeFormerTypeLevelQuick type with
-  | .some l => return .some l
-  | .none => savingCache <| go type #[]
-where
-  go (type : Expr) (xs : Array Expr) : MetaM (Option Level) := do
-    match type with
-    | .sort l => return some l
-    | .forallE n d b c => withLocalDecl' n c (d.instantiateRev xs) fun x => go b (xs.push x)
-    | _ =>
-      let type ← whnfD (type.instantiateRev xs)
-      match type with
-      | .sort l => return some l
-      | .forallE .. => go type #[]
-      | _ => return none
+def isTypeFormerTypeQuick : Expr → Bool
+  | .forallE _ _ b _ => isTypeFormerTypeQuick b
+  | .sort _ => true
+  | _ => false
 
 /--
 Return true iff `type` is `Sort _` or `As → Sort _`.
 -/
 partial def isTypeFormerType (type : Expr) : MetaM Bool := do
-  return (← typeFormerTypeLevel type).isSome
-
-/--
-Return true iff `type` is `Prop` or `As → Prop`.
--/
-partial def isPropFormerType (type : Expr) : MetaM Bool := do
-  return (← typeFormerTypeLevel type) == .some .zero
+  match isTypeFormerTypeQuick type with
+  | true => return true
+  | false => savingCache <| go type #[]
+where
+  go (type : Expr) (xs : Array Expr) : MetaM Bool := do
+    match type with
+    | .sort .. => return true
+    | .forallE n d b c => withLocalDecl' n c (d.instantiateRev xs) fun x => go b (xs.push x)
+    | _ =>
+      let type ← whnfD (type.instantiateRev xs)
+      match type with
+      | .sort .. => return true
+      | .forallE .. => go type #[]
+      | _ => return false
 
 /--
 Return true iff `e : Sort _` or `e : (forall As, Sort _)`.