restore newly-confluence #check_simp

.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/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/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
@@ -883,8 +880,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 +899,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 -/

src/Init/Data/List/Lemmas.lean

@@ -33,23 +33,6 @@ For each `List` operation, we would like theorems describing the following, when
 
 Of course for any individual operation, not all of these will be relevant or helpful, so some judgement is required.
 
-General principles for `simp` normal forms for `List` operations:
-* Conversion operations (e.g. `toArray`, or `length`) should be moved inwards aggressively,
-  to make the conversion effective.
-* Similarly, operation which work on elements should be moved inwards in preference to
-  "structural" operations on the list, e.g. we prefer to simplify
-  `List.map f (L ++ M) ~> (List.map f L) ++ (List.map f M)`,
-  `List.map f L.reverse ~> (List.map f L).reverse`, and
-  `List.map f (L.take n) ~> (List.map f L).take n`.
-* Arithmetic operations are "light", so e.g. we prefer to simplify `drop i (drop j L)` to `drop (i + j) L`,
-  rather than the other way round.
-* Function compositions are "light", so we prefer to simplify `(L.map f).map g` to `L.map (g ∘ f)`.
-* We try to avoid non-linear left hand sides (i.e. with subexpressions appearing multiple times),
-  but this is only a weak preference.
-* Generally, we prefer that the right hand side does not introduce duplication,
-  however generally duplication of higher order arguments (functions, predicates, etc) is allowed,
-  as we expect to be able to compute these once they reach ground terms.
-
 -/
 namespace List
 
@@ -175,7 +158,7 @@ theorem getElem?_len_le : ∀ {l : List α} {n}, length l ≤ n → l[n]? = none
   | _ :: l, _+1, h => by
     rw [getElem?_cons_succ, getElem?_len_le (l := l) <| Nat.le_of_succ_le_succ h]
 
-@[simp] theorem getElem?_eq_getElem {l : List α} {n} (h : n < l.length) : l[n]? = some l[n] := by
+theorem getElem?_eq_getElem {l : List α} {n} (h : n < l.length) : l[n]? = some l[n] := by
   simp only [← get?_eq_getElem?, get?_eq_get, h, get_eq_getElem]
 
 theorem getElem?_eq_some {l : List α} : l[n]? = some a ↔ ∃ h : n < l.length, l[n] = a := by
@@ -268,12 +251,9 @@ theorem ext_get {l₁ l₂ : List α} (hl : length l₁ = length l₂)
     (h : ∀ n h₁ h₂, get l₁ ⟨n, h₁⟩ = get l₂ ⟨n, h₂⟩) : l₁ = l₂ :=
   ext_getElem hl (by simp_all)
 
-@[simp] theorem getElem_concat_length : ∀ (l : List α) (a : α) (i) (_ : i = l.length) (w), (l ++ [a])[i]'w = a
-  | [], a, _, h, _ => by subst h; simp
-  | _ :: l, a, _, h, _ => by simp [getElem_concat_length, h]
-
-theorem getElem?_concat_length (l : List α) (a : α) : (l ++ [a])[l.length]? = some a := by
-  simp
+@[simp] theorem getElem?_concat_length : ∀ (l : List α) (a : α), (l ++ [a])[l.length]? = some a
+  | [], a => rfl
+  | b :: l, a => by rw [cons_append, length_cons]; simp [getElem?_concat_length]
 
 @[deprecated getElem?_concat_length (since := "2024-06-12")]
 theorem get?_concat_length (l : List α) (a : α) : (l ++ [a]).get? l.length = some a := by simp
@@ -607,20 +587,6 @@ theorem foldr_map (f : α₁ → α₂) (g : α₂ → β → β) (l : List α
     (l.map f).foldr g init = l.foldr (fun x y => g (f x) y) init := by
   induction l generalizing init <;> simp [*]
 
-theorem foldl_map' {α β : Type u} (g : α → β) (f : α → α → α) (f' : β → β → β) (a : α) (l : List α)
-    (h : ∀ x y, f' (g x) (g y) = g (f x y)) :
-    (l.map g).foldl f' (g a) = g (l.foldl f a) := by
-  induction l generalizing a
-  · simp
-  · simp [*, h]
-
-theorem foldr_map' {α β : Type u} (g : α → β) (f : α → α → α) (f' : β → β → β) (a : α) (l : List α)
-    (h : ∀ x y, f' (g x) (g y) = g (f x y)) :
-    (l.map g).foldr f' (g a) = g (l.foldr f a) := by
-  induction l generalizing a
-  · simp
-  · simp [*, h]
-
 /-! ### getD -/
 
 @[simp] theorem getD_eq_getElem? (l) (n) (a : α) : getD l n a = (l[n]?).getD a := by
@@ -713,15 +679,6 @@ theorem head?_eq_head : ∀ l h, @head? α l = some (head l h)
 
 /-! ### map -/
 
-@[simp] theorem map_id (l : List α) : map id l = l := by induction l <;> simp_all
-
-@[simp] theorem map_id' (l : List α) : map (fun a => a) l = l := by induction l <;> simp_all
-
-theorem map_id'' {f : α → α} (h : ∀ x, f x = x) (l : List α) : map f l = l := by
-  simp [show f = id from funext h]
-
-theorem map_singleton (f : α → β) (a : α) : map f [a] = [f a] := rfl
-
 @[simp] theorem length_map (as : List α) (f : α → β) : (as.map f).length = as.length := by
   induction as with
   | nil => simp [List.map]
@@ -747,105 +704,33 @@ theorem get_map (f : α → β) {l n} :
     get (map f l) n = f (get l ⟨n, length_map l f ▸ n.2⟩) := by
   simp
 
+@[simp] theorem map_append (f : α → β) : ∀ l₁ l₂, map f (l₁ ++ l₂) = map f l₁ ++ map f l₂ := by
+  intro l₁; induction l₁ <;> intros <;> simp_all
+
+@[simp] theorem map_id (l : List α) : map id l = l := by induction l <;> simp_all
+
+@[simp] theorem map_id' (l : List α) : map (fun a => a) l = l := by induction l <;> simp_all
+
 @[simp] theorem mem_map {f : α → β} : ∀ {l : List α}, b ∈ l.map f ↔ ∃ a, a ∈ l ∧ f a = b
   | [] => by simp
   | _ :: l => by simp [mem_map (l := l), eq_comm (a := b)]
 
-theorem exists_of_mem_map (h : b ∈ map f l) : ∃ a, a ∈ l ∧ f a = b := mem_map.1 h
-
 theorem mem_map_of_mem (f : α → β) (h : a ∈ l) : f a ∈ map f l := mem_map.2 ⟨_, h, rfl⟩
 
-@[simp] theorem map_inj_left {f g : α → β} : map f l = map g l ↔ ∀ a ∈ l, f a = g a := by
-  induction l <;> simp_all
-
-theorem map_congr_left (h : ∀ a ∈ l, f a = g a) : map f l = map g l :=
-  map_inj_left.2 h
-
-theorem map_inj : map f = map g ↔ f = g := by
-  constructor
-  · intro h; ext a; replace h := congrFun h [a]; simpa using h
-  · intro h; subst h; rfl
-
-@[simp] theorem map_eq_nil {f : α → β} {l : List α} : map f l = [] ↔ l = [] := by
-  constructor <;> exact fun _ => match l with | [] => rfl
-
-theorem eq_nil_of_map_eq_nil {f : α → β} {l : List α} (h : map f l = []) : l = [] :=
-  map_eq_nil.mp h
-
-theorem map_eq_cons {f : α → β} {l : List α} :
-    map f l = b :: l₂ ↔ l.head?.map f = some b ∧ l.tail?.map (map f) = some l₂ := by
-  induction l <;> simp_all
-
-theorem map_eq_cons' {f : α → β} {l : List α} :
-    map f l = b :: l₂ ↔ ∃ a l₁, l = a :: l₁ ∧ f a = b ∧ map f l₁ = l₂ := by
-  cases l
-  case nil => simp
-  case cons a l₁ =>
-    simp only [map_cons, cons.injEq]
-    constructor
-    · rintro ⟨rfl, rfl⟩
-      exact ⟨a, l₁, ⟨rfl, rfl⟩, ⟨rfl, rfl⟩⟩
-    · rintro ⟨a, l₁, ⟨rfl, rfl⟩, ⟨rfl, rfl⟩⟩
-      constructor <;> rfl
-
-theorem map_eq_foldr (f : α → β) (l : List α) : map f l = foldr (fun a bs => f a :: bs) [] l := by
-  induction l <;> simp [*]
-
-@[simp] theorem set_map {f : α → β} {l : List α} {n : Nat} {a : α} :
-    (map f l).set n (f a) = map f (l.set n a) := by
-  induction l generalizing n with
-  | nil => simp
-  | cons b l ih => cases n <;> simp_all
-
-@[simp] theorem head_map (f : α → β) (l : List α) (w) :
-    head (map f l) w = f (head l (by simpa using w)) := by
-  cases l
-  · simp at w
-  · simp_all
-
-@[simp] theorem head?_map (f : α → β) (l : List α) : head? (map f l) = (head? l).map f := by
-  cases l <;> rfl
-
-@[simp] theorem headD_map (f : α → β) (l : List α) (a : α) : headD (map f l) (f a) = f (headD l a) := by
-  cases l <;> rfl
-
-@[simp] theorem tail?_map (f : α → β) (l : List α) : tail? (map f l) = (tail? l).map (map f) := by
-  cases l <;> rfl
-
-@[simp] theorem tailD_map (f : α → β) (l : List α) (l' : List α) :
-    tailD (map f l) (map f l') = map f (tailD l l') := by
-  cases l <;> rfl
-
-@[simp] theorem getLast_map (f : α → β) (l : List α) (h) :
-    getLast (map f l) h = f (getLast l (by simpa using h)) := by
-  cases l
-  · simp at h
-  · simp only [← getElem_cons_length _ _ _ rfl]
-    simp only [map_cons]
-    simp only [← getElem_cons_length _ _ _ rfl]
-    simp only [← map_cons, getElem_map]
-    simp
-
-@[simp] theorem getLast?_map (f : α → β) (l : List α) : getLast? (map f l) = (getLast? l).map f := by
-  cases l
-  · simp
-  · rw [getLast?_eq_getLast, getLast?_eq_getLast, getLast_map] <;> simp
-
-@[simp] theorem getLastD_map (f : α → β) (l : List α) (a : α) : getLastD (map f l) (f a) = f (getLastD l a) := by
-  cases l
-  · simp
-  · rw [getLastD_eq_getLast?, getLastD_eq_getLast?, getLast?_map] <;> simp
-
-@[simp] theorem map_append (f : α → β) : ∀ l₁ l₂, map f (l₁ ++ l₂) = map f l₁ ++ map f l₂ := by
-  intro l₁; induction l₁ <;> intros <;> simp_all
-
 @[simp] theorem map_map (g : β → γ) (f : α → β) (l : List α) :
   map g (map f l) = map (g ∘ f) l := by induction l <;> simp_all
 
+theorem map_singleton (f : α → β) (a : α) : map f [a] = [f a] := rfl
+
+theorem exists_of_mem_map (h : b ∈ map f l) : ∃ a, a ∈ l ∧ f a = b := mem_map.1 h
+
 theorem forall_mem_map_iff {f : α → β} {l : List α} {P : β → Prop} :
     (∀ (i) (_ : i ∈ l.map f), P i) ↔ ∀ (j) (_ : j ∈ l), P (f j) := by
   simp
 
+@[simp] theorem map_eq_nil {f : α → β} {l : List α} : map f l = [] ↔ l = [] := by
+  constructor <;> exact fun _ => match l with | [] => rfl
+
 /-! ### filter -/
 
 @[simp] theorem filter_cons_of_pos {p : α → Bool} {a : α} (l) (pa : p a) :
@@ -909,28 +794,18 @@ theorem filter_map (f : β → α) (l : List β) : filter p (map f l) = map f (f
 
 @[deprecated filter_map (since := "2024-06-15")] abbrev map_filter := @filter_map
 
-theorem map_filter_eq_foldr (f : α → β) (p : α → Bool) (as : List α) :
-    map f (filter p as) = foldr (fun a bs => bif p a then f a :: bs else bs) [] as := by
-  induction as with
-  | nil => rfl
-  | cons head _ ih =>
-    simp only [foldr]
-    cases hp : p head <;> simp [filter, *]
-
 @[simp] theorem filter_append {p : α → Bool} :
     ∀ (l₁ l₂ : List α), filter p (l₁ ++ l₂) = filter p l₁ ++ filter p l₂
   | [], l₂ => rfl
   | a :: l₁, l₂ => by simp [filter]; split <;> simp [filter_append l₁]
 
-theorem filter_congr {p q : α → Bool} :
-    ∀ {l : List α}, (∀ x ∈ l, p x = q x) → filter p l = filter q l
+theorem filter_congr' {p q : α → Bool} :
+    ∀ {l : List α}, (∀ x ∈ l, p x ↔ q x) → filter p l = filter q l
   | [], _ => rfl
   | a :: l, h => by
     rw [forall_mem_cons] at h; by_cases pa : p a
-    · simp [pa, h.1 ▸ pa, filter_congr h.2]
-    · simp [pa, h.1 ▸ pa, filter_congr h.2]
-
-@[deprecated filter_congr (since := "2024-06-20")] abbrev filter_congr' := @filter_congr
+    · simp [pa, h.1.1 pa, filter_congr' h.2]
+    · simp [pa, mt h.1.2 pa, filter_congr' h.2]
 
 /-! ### filterMap -/
 
@@ -1218,11 +1093,6 @@ theorem concat_append (a : α) (l₁ l₂ : List α) : concat l₁ a ++ l₂ = l
 
 theorem append_concat (a : α) (l₁ l₂ : List α) : l₁ ++ concat l₂ a = concat (l₁ ++ l₂) a := by simp
 
-theorem map_concat (f : α → β) (a : α) (l : List α) : map f (concat l a) = concat (map f l) (f a) := by
-  induction l with
-  | nil => rfl
-  | cons x xs ih => simp [ih]
-
 theorem eq_nil_or_concat : ∀ l : List α, l = [] ∨ ∃ L b, l = concat L b
   | [] => .inl rfl
   | a::l => match l, eq_nil_or_concat l with
@@ -1239,9 +1109,6 @@ theorem exists_of_mem_join : a ∈ join L → ∃ l, l ∈ L ∧ a ∈ l := mem_
 
 theorem mem_join_of_mem (lL : l ∈ L) (al : a ∈ l) : a ∈ join L := mem_join.2 ⟨l, lL, al⟩
 
-@[simp] theorem map_join (f : α → β) (L : List (List α)) : map f (join L) = join (map (map f) L) := by
-  induction L <;> simp_all
-
 /-! ### bind -/
 
 @[simp] theorem append_bind xs ys (f : α → List β) :
@@ -1260,27 +1127,10 @@ theorem exists_of_mem_bind {b : β} {l : List α} {f : α → List β} :
 theorem mem_bind_of_mem {b : β} {l : List α} {f : α → List β} {a} (al : a ∈ l) (h : b ∈ f a) :
     b ∈ List.bind l f := mem_bind.2 ⟨a, al, h⟩
 
-theorem bind_singleton (f : α → List β) (x : α) : [x].bind f = f x :=
-  append_nil (f x)
-
-@[simp] theorem bind_singleton' (l : List α) : (l.bind fun x => [x]) = l := by
-  induction l <;> simp [*]
-
-theorem bind_assoc {α β} (l : List α) (f : α → List β) (g : β → List γ) :
-    (l.bind f).bind g = l.bind fun x => (f x).bind g := by
-  induction l <;> simp [*]
-
-theorem map_bind (f : β → γ) (g : α → List β) :
-    ∀ l : List α, (l.bind g).map f = l.bind fun a => (g a).map f
+theorem bind_map (f : β → γ) (g : α → List β) :
+    ∀ l : List α, map f (l.bind g) = l.bind fun a => (g a).map f
   | [] => rfl
-  | a::l => by simp only [bind_cons, map_append, map_bind _ _ l]
-
-theorem bind_map (f : α → β) (g : β → List γ) (l : List α) : (map f l).bind g = l.bind (fun a => g (f a)) := by
-  induction l <;> simp [bind_cons, append_bind, *]
-
-theorem map_eq_bind {α β} (f : α → β) (l : List α) : map f l = l.bind fun x => [f x] := by
-  simp only [← map_singleton]
-  rw [← bind_singleton' l, map_bind, bind_singleton']
+  | a::l => by simp only [bind_cons, map_append, bind_map _ _ l]
 
 /-! ### replicate -/
 
@@ -1349,17 +1199,6 @@ theorem eq_replicate {a : α} {n} {l : List α} :
   ⟨fun h => h ▸ ⟨length_replicate .., fun _ => eq_of_mem_replicate⟩,
    fun ⟨e, al⟩ => e ▸ eq_replicate_of_mem al⟩
 
-theorem map_eq_replicate_iff {l : List α} {f : α → β} {b : β} :
-    l.map f = replicate l.length b ↔ ∀ x ∈ l, f x = b := by
-  simp [eq_replicate]
-
-@[simp] theorem map_const (l : List α) (b : β) : map (Function.const α b) l = replicate l.length b :=
-  map_eq_replicate_iff.mpr fun _ _ => rfl
-
--- This can not be a `@[simp]` lemma because it would fire on every `List.map`.
-theorem map_const' (l : List α) (b : β) : map (fun _ => b) l = replicate l.length b :=
-  map_const l b
-
 @[simp] theorem append_replicate_replicate : replicate n a ++ replicate m a = replicate (n + m) a := by
   rw [eq_replicate]
   constructor
@@ -1477,12 +1316,8 @@ theorem reverseAux_reverseAux_nil (as bs : List α) : reverseAux (reverseAux as
 @[simp] theorem reverse_append (as bs : List α) : (as ++ bs).reverse = bs.reverse ++ as.reverse := by
   induction as <;> simp_all
 
-@[simp] theorem map_reverse (f : α → β) (l : List α) : l.reverse.map f = (l.map f).reverse := by
-  induction l <;> simp [*]
-
-@[deprecated map_reverse (since := "2024-06-20")]
 theorem reverse_map (f : α → β) (l : List α) : (l.map f).reverse = l.reverse.map f := by
-  simp
+  induction l <;> simp [*]
 
 @[simp] theorem reverse_eq_nil_iff {xs : List α} : xs.reverse = [] ↔ xs = [] := by
   match xs with
@@ -1516,11 +1351,13 @@ theorem reverseAux_eq (as bs : List α) : reverseAux as bs = reverse as ++ bs :=
 
 /-! ## List membership -/
 
-/-! ### elem / contains -/
+/-! ### elem -/
 
 @[simp] theorem elem_cons_self [BEq α] [LawfulBEq α] {a : α} : (a::as).elem a = true := by
   simp [elem_cons]
 
+/-! ### contains -/
+
 @[simp] theorem contains_cons [BEq α] :
     (a :: as : List α).contains x = (x == a || as.contains x) := by
   simp only [contains, elem]
@@ -1581,7 +1418,7 @@ theorem take_left : ∀ l₁ l₂ : List α, take (length l₁) (l₁ ++ l₂) =
 theorem take_left' {l₁ l₂ : List α} {n} (h : length l₁ = n) : take n (l₁ ++ l₂) = l₁ := by
   rw [← h]; apply take_left
 
-@[simp] theorem map_take (f : α → β) :
+theorem map_take (f : α → β) :
     ∀ (L : List α) (i : Nat), (L.take i).map f = (L.map f).take i
   | [], i => by simp
   | _, 0 => by simp
@@ -1670,7 +1507,7 @@ theorem take_drop : ∀ (m n : Nat) (l : List α), take n (drop m l) = drop m (t
   | _, _, [] => by simp
   | _+1, _, _ :: _ => by simpa [Nat.succ_add, take_succ_cons, drop_succ_cons] using take_drop ..
 
-@[simp] theorem map_drop (f : α → β) :
+theorem map_drop (f : α → β) :
     ∀ (L : List α) (i : Nat), (L.drop i).map f = (L.map f).drop i
   | [], i => by simp
   | L, 0 => by simp
@@ -1724,22 +1561,6 @@ theorem dropWhile_cons :
     (x :: xs : List α).dropWhile p = if p x then xs.dropWhile p else x :: xs := by
   split <;> simp_all [dropWhile]
 
-theorem takeWhile_map (f : α → β) (p : β → Bool) (l : List α) :
-    (l.map f).takeWhile p = (l.takeWhile (p ∘ f)).map f := by
-  induction l with
-  | nil => rfl
-  | cons x xs ih =>
-    simp only [map_cons, takeWhile_cons]
-    split <;> simp_all
-
-theorem dropWhile_map (f : α → β) (p : β → Bool) (l : List α) :
-    (l.map f).dropWhile p = (l.dropWhile (p ∘ f)).map f := by
-  induction l with
-  | nil => rfl
-  | cons x xs ih =>
-    simp only [map_cons, dropWhile_cons]
-    split <;> simp_all
-
 @[simp] theorem takeWhile_append_dropWhile (p : α → Bool) :
     ∀ (l : List α), takeWhile p l ++ dropWhile p l = l
   | [] => rfl
@@ -1824,11 +1645,6 @@ theorem dropLast_append_cons : dropLast (l₁ ++ b::l₂) = l₁ ++ dropLast (b:
 
 @[simp 1100] theorem dropLast_concat : dropLast (l₁ ++ [b]) = l₁ := by simp
 
-@[simp] theorem map_dropLast (f : α → β) (l : List α) : l.dropLast.map f = (l.map f).dropLast := by
-  induction l with
-  | nil => rfl
-  | cons x xs ih => cases xs <;> simp [ih]
-
 @[simp] theorem dropLast_replicate (n) (a : α) : dropLast (replicate n a) = replicate (n - 1) a := by
   match n with
   | 0 => simp
@@ -1881,17 +1697,11 @@ end isSuffixOf
 @[simp] theorem rotateLeft_zero (l : List α) : rotateLeft l 0 = l := by
   simp [rotateLeft]
 
--- TODO Batteries defines its own `getElem?_rotate`, which we need to adapt.
--- TODO Prove `map_rotateLeft`, using `ext` and `getElem?_rotateLeft`.
-
 /-! ### rotateRight -/
 
 @[simp] theorem rotateRight_zero (l : List α) : rotateRight l 0 = l := by
   simp [rotateRight]
 
--- TODO Batteries defines its own `getElem?_rotate`, which we need to adapt.
--- TODO Prove `map_rotateRight`, using `ext` and `getElem?_rotateRight`.
-
 /-! ## Manipulating elements -/
 
 /-! ### replace -/
@@ -2014,13 +1824,6 @@ theorem find?_some : ∀ {l}, find? p l = some a → p a
     · exact H ▸ .head _
     · exact .tail _ (mem_of_find?_eq_some H)
 
-@[simp] theorem find?_map (f : β → α) (l : List β) : find? p (l.map f) = (l.find? (p ∘ f)).map f := by
-  induction l with
-  | nil => simp
-  | cons x xs ih =>
-    simp only [map_cons, find?]
-    by_cases h : p (f x) <;> simp [h, ih]
-
 theorem find?_replicate : find? p (replicate n a) = if n = 0 then none else if p a then some a else none := by
   cases n
   · simp
@@ -2053,13 +1856,6 @@ theorem exists_of_findSome?_eq_some {l : List α} {f : α → Option β} (w : l.
     simp_all only [findSome?_cons, mem_cons, exists_eq_or_imp]
     split at w <;> simp_all
 
-@[simp] theorem findSome?_map (f : β → γ) (l : List β) : findSome? p (l.map f) = l.findSome? (p ∘ f) := by
-  induction l with
-  | nil => simp
-  | cons x xs ih =>
-    simp only [map_cons, findSome?]
-    split <;> simp_all
-
 theorem findSome?_replicate : findSome? f (replicate n a) = if n = 0 then none else f a := by
   induction n with
   | zero => simp
@@ -2142,12 +1938,6 @@ theorem any_eq_not_all_not (l : List α) (p : α → Bool) : l.any p = !l.all (!
 theorem all_eq_not_any_not (l : List α) (p : α → Bool) : l.all p = !l.any (!p .) := by
   simp only [not_any_eq_all_not, Bool.not_not]
 
-theorem any_map (f : α → β) (l : List α) (p : β → Bool) : (l.map f).any p = l.any (p ∘ f) := by
-  induction l with simp | cons _ _ ih => rw [ih]
-
-theorem all_map (f : α → β) (l : List α) (p : β → Bool) : (l.map f).all p = l.all (p ∘ f) := by
-  induction l with simp | cons _ _ ih => rw [ih]
-
 /-! ## Zippers -/
 
 /-! ### zip -/
@@ -2334,25 +2124,6 @@ theorem get?_zipWithAll {f : Option α → Option β → γ} :
 set_option linter.deprecated false in
 @[deprecated getElem?_zipWithAll (since := "2024-06-07")] abbrev zipWithAll_get? := @get?_zipWithAll
 
-theorem zipWithAll_map {μ} (f : Option γ → Option δ → μ) (g : α → γ) (h : β → δ) (l₁ : List α) (l₂ : List β) :
-    zipWithAll f (l₁.map g) (l₂.map h) = zipWithAll (fun a b => f (g <$> a) (h <$> b)) l₁ l₂ := by
-  induction l₁ generalizing l₂ <;> cases l₂ <;> simp_all
-
-theorem zipWithAll_map_left (l₁ : List α) (l₂ : List β) (f : α → α') (g : Option α' → Option β → γ) :
-    zipWithAll g (l₁.map f) l₂ = zipWithAll (fun a b => g (f <$> a) b) l₁ l₂ := by
-  induction l₁ generalizing l₂ <;> cases l₂ <;> simp_all
-
-theorem zipWithAll_map_right (l₁ : List α) (l₂ : List β) (f : β → β') (g : Option α → Option β' → γ) :
-    zipWithAll g l₁ (l₂.map f) = zipWithAll (fun a b => g a (f <$> b)) l₁ l₂ := by
-  induction l₁ generalizing l₂ <;> cases l₂ <;> simp_all
-
-theorem map_zipWithAll {δ : Type _} (f : α → β) (g : Option γ → Option δ → α) (l : List γ) (l' : List δ) :
-    map f (zipWithAll g l l') = zipWithAll (fun x y => f (g x y)) l l' := by
-  induction l generalizing l' with
-  | nil => simp
-  | cons hd tl hl =>
-    cases l' <;> simp_all
-
 @[simp] theorem zipWithAll_replicate {a : α} {b : β} {n : Nat} :
     zipWithAll f (replicate n a) (replicate n b) = replicate n (f a b) := by
   induction n with
@@ -2375,10 +2146,6 @@ theorem map_zipWithAll {δ : Type _} (f : α → β) (g : Option γ → Option
   | _, [] => rfl
   | _, _ :: _ => congrArg Nat.succ enumFrom_length
 
-theorem map_enumFrom (f : α → β) (n : Nat) (l : List α) :
-    map (Prod.map id f) (enumFrom n l) = enumFrom n (map f l) := by
-  induction l generalizing n <;> simp_all
-
 /-! ### enum -/
 
 @[simp] theorem enum_length : (enum l).length = l.length :=
@@ -2386,9 +2153,6 @@ theorem map_enumFrom (f : α → β) (n : Nat) (l : List α) :
 
 theorem enum_cons : (a::as).enum = (0, a) :: as.enumFrom 1 := rfl
 
-theorem map_enum (f : α → β) (l : List α) : map (Prod.map id f) (enum l) = enum (map f l) :=
-  map_enumFrom f 0 l
-
 /-! ## Minima and maxima -/
 
 /-! ### minimum? -/

src/Init/Data/List/TakeDrop.lean

@@ -316,7 +316,7 @@ theorem take_reverse {α} {xs : List α} (n : Nat) (h : n ≤ xs.length) :
     have : (n + 1) % m < m := Nat.mod_lt _ (by omega)
     omega
 
-/-! ### rotateRight -/
+/-! ### rotateLeft -/
 
 @[simp] theorem rotateRight_replicate (n) (a : α) : rotateRight (replicate m a) n = replicate m a := by
   cases n with
@@ -364,24 +364,4 @@ theorem zip_eq_zip_take_min : ∀ (l₁ : List α) (l₂ : List β),
   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

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/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/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/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/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)

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/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/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,7 +150,7 @@ 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
@@ -189,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
@@ -208,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
@@ -231,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 =>
@@ -240,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]
@@ -321,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/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/MutualDef.lean

@@ -846,10 +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
-      -- Remark: we should consider using `pure view.kind.isTheorem <||> isProp header.type`, and
-      -- also handle definitions. We used the following approach because it is less disruptive to Mathlib.
-      -- Moreover, the type of most definitions are not propositions anyway.
-      if ← pure view.kind.isTheorem <||> (pure view.kind.isExample <&&> 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/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/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 =>
@@ -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)
 

src/Lean/Environment.lean

@@ -423,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
@@ -628,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 _ => {},
@@ -1013,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);
@@ -1089,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,93 +7,33 @@ prelude
 import Lean.AuxRecursor
 import Lean.AddDecl
 import Lean.Meta.AppBuilder
-import Lean.Meta.CompletionName
-import Lean.Meta.Constructions.RecOn
 
 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_below"] opaque mkBelowImp (env : Environment) (declName : @& Name) (ibelow : Bool) : Except KernelException Declaration
-@[extern "lean_mk_brec_on"] opaque mkBRecOnImp (env : Environment) (declName : @& Name) (ind : Bool) : 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
-
-private def mkBelowOrIBelow (declName : Name) (ibelow : Bool) : MetaM Unit := do
-  let .inductInfo indVal ← getConstInfo declName | return
-  unless indVal.isRec do return
-  if ← isPropFormerType indVal.type then return
-
-  let decl ← ofExceptKernelException (mkBelowImp (← getEnv) declName ibelow)
-  let name := decl.definitionVal!.name
-  addDecl decl
-  setReducibleAttribute name
-  modifyEnv fun env => addToCompletionBlackList env name
-  modifyEnv fun env => addProtected env name
-
-def mkBelow (declName : Name) : MetaM Unit := mkBelowOrIBelow declName true
-def mkIBelow (declName : Name) : MetaM Unit := mkBelowOrIBelow declName false
-
-private def mkBRecOrBInductionOn (declName : Name) (ind : Bool) : MetaM Unit := do
-  let .inductInfo indVal ← getConstInfo declName | return
-  unless indVal.isRec do return
-  if ← isPropFormerType indVal.type then return
-  let .recInfo recInfo ← getConstInfo (mkRecName declName) | return
-  unless recInfo.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 decl ← ofExceptKernelException (mkBRecOnImp (← getEnv) declName ind)
-  let name := decl.definitionVal!.name
-  addDecl decl
-  setReducibleAttribute name
-  modifyEnv fun env => markAuxRecursor env name
-  modifyEnv fun env => addProtected env name
-
-def mkBRecOn (declName : Name) : MetaM Unit := mkBRecOrBInductionOn declName false
-def mkBInductionOn (declName : Name) : MetaM Unit := mkBRecOrBInductionOn declName true
-
-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

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/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 _)`.

src/Lean/Meta/Match/Match.lean

@@ -776,8 +776,14 @@ def mkMatcherAuxDefinition (name : Name) (type : Expr) (value : Expr) : MetaM (E
   match (matcherExt.getState env).find? (result.value, compile) with
   | some nameNew => return (mkMatcherConst nameNew, none)
   | none =>
-    let decl := Declaration.defnDecl (← mkDefinitionValInferrringUnsafe name result.levelParams.toList
-      result.type result.value .abbrev)
+    let decl := Declaration.defnDecl {
+      name
+      levelParams := result.levelParams.toList
+      type        := result.type
+      value       := result.value
+      hints       := ReducibilityHints.abbrev
+      safety      := if env.hasUnsafe result.type || env.hasUnsafe result.value then DefinitionSafety.unsafe else DefinitionSafety.safe
+    }
     trace[Meta.Match.debug] "{name} : {result.type} := {result.value}"
     let addMatcher : MatcherInfo → MetaM Unit := fun mi => do
       addDecl decl

src/Lean/Meta/SynthInstance.lean

@@ -194,6 +194,9 @@ def checkSystem : SynthM Unit := do
   Core.checkInterrupted
   Core.checkMaxHeartbeatsCore "typeclass" `synthInstance.maxHeartbeats (← read).maxHeartbeats
 
+@[inline] def mapMetaM (f : forall {α}, MetaM α → MetaM α) {α} : SynthM α → SynthM α :=
+  monadMap @f
+
 instance : Inhabited (SynthM α) where
   default := fun _ _ => default
 
@@ -333,6 +336,26 @@ def getSubgoals (lctx : LocalContext) (localInsts : LocalInstances) (xs : Array
     subgoals := inst.synthOrder.map (mvars[·]!) |>.toList
   }
 
+/--
+Similar to `mkLambdaFVars`, but ensures result is eta-reduced.
+For example, suppose `e` is the local variable `inst x y`, and `xs` is `#[x, y]`, then
+the result is `inst` instead of `fun x y => inst x y`.
+
+We added this auxiliary function because of aliases such as `DecidablePred`. For example,
+consider the following definition.
+```
+def filter (p : α → Prop) [inst : DecidablePred p] (xs : List α) : List α :=
+  match xs with
+  | [] => []
+  | x :: xs' => if p x then x :: filter p xs' else filter p xs'
+```
+Without `mkLambdaFVars'`, the implicit instance at the `filter` applications would be `fun x => inst x` instead of `inst`.
+Moreover, the equation lemmas associated with `filter` would have `fun x => inst x` on their right-hand-side. Then,
+we would start getting terms such as `fun x => (fun x => inst x) x` when using the equational theorem.
+-/
+private def mkLambdaFVars' (xs : Array Expr) (e : Expr) : MetaM Expr :=
+  return (← mkLambdaFVars xs e).eta
+
 /--
   Try to synthesize metavariable `mvar` using the instance `inst`.
   Remark: `mctx` is set using `withMCtx`.
@@ -350,23 +373,7 @@ def tryResolve (mvar : Expr) (inst : Instance) : MetaM (Option (MetavarContext
     withTraceNode `Meta.synthInstance.tryResolve (withMCtx (← getMCtx) do
         return m!"{exceptOptionEmoji ·} {← instantiateMVars mvarTypeBody} ≟ {← instantiateMVars instTypeBody}") do
     if (← isDefEq mvarTypeBody instTypeBody) then
-      /-
-      We set `etaReduce := true`.
-      For example, suppose `e` is the local variable `inst x y`, and `xs` is `#[x, y]`, then
-      the result is `inst` instead of `fun x y => inst x y`.
-
-      Consider the following definition.
-      ```
-      def filter (p : α → Prop) [inst : DecidablePred p] (xs : List α) : List α :=
-        match xs with
-        | [] => []
-        | x :: xs' => if p x then x :: filter p xs' else filter p xs'
-      ```
-      Without `etaReduce := true`, the implicit instance at the `filter` applications would be `fun x => inst x` instead of `inst`.
-      Moreover, the equation lemmas associated with `filter` would have `fun x => inst x` on their right-hand-side. Then,
-      we would start getting terms such as `fun x => (fun x => inst x) x` when using the equational theorem.
-      -/
-      let instVal ← mkLambdaFVars xs instVal (etaReduce := true)
+      let instVal ← mkLambdaFVars' xs instVal
       if (← isDefEq mvar instVal) then
         return some ((← getMCtx), subgoals)
     return none
@@ -479,7 +486,7 @@ private def removeUnusedArguments? (mctx : MetavarContext) (mvar : Expr) : MetaM
         let ys := ys.toArray
         let mvarType' ← mkForallFVars ys body
         withLocalDeclD `redf mvarType' fun f => do
-          let transformer ← mkLambdaFVars #[f] (← mkLambdaFVars xs (mkAppN f ys) (etaReduce := true)) (etaReduce := true)
+          let transformer ← mkLambdaFVars' #[f] (← mkLambdaFVars' xs (mkAppN f ys))
           trace[Meta.synthInstance.unusedArgs] "{mvarType}\nhas unused arguments, reduced type{indentExpr mvarType'}\nTransformer{indentExpr transformer}"
           return some (mvarType', transformer)
 
@@ -698,83 +705,6 @@ private def preprocessOutParam (type : Expr) : MetaM Expr :=
   Remark: we use a different option for controlling the maximum result size for coercions.
 -/
 
-private def assignOutParams (type : Expr) (result : Expr) : MetaM Bool := do
-  let resultType ← inferType result
-  /- Output parameters of local instances may be marked as `syntheticOpaque` by the application-elaborator.
-      We use `withAssignableSyntheticOpaque` to make sure this kind of parameter can be assigned by the following `isDefEq`.
-      TODO: rewrite this check to avoid `withAssignableSyntheticOpaque`. -/
-  let defEq ← withDefault <| withAssignableSyntheticOpaque <| isDefEq type resultType
-  unless defEq do
-    trace[Meta.synthInstance] "{crossEmoji} result type{indentExpr resultType}\nis not definitionally equal to{indentExpr type}"
-  return defEq
-
-/--
-Auxiliary function for converting the `AbstractMVarsResult` returned by `SynthIntance.main` into an `Expr`.
--/
-private def applyAbstractResult? (type : Expr) (abstResult? : Option AbstractMVarsResult) : MetaM (Option Expr) := do
-  let some abstResult := abstResult? | return none
-  let (_, _, result) ← openAbstractMVarsResult abstResult
-  unless (← assignOutParams type result) do return none
-  let result ← instantiateMVars result
-  /- We use `check` to propagate universe constraints implied by the `result`.
-      Recall that we use `allowLevelAssignments := true` which allows universe metavariables in the current depth to be assigned,
-      but these assignments are discarded by `withNewMCtxDepth`.
-
-      TODO: If this `check` is a performance bottleneck, we can improve performance by tracking whether
-            a universe metavariable from previous universe levels have been assigned or not during TC resolution.
-            We only need to perform the `check` if this kind of assignment have been performed.
-
-      The example in the issue #796 exposed this issue.
-      ```
-      structure A
-      class B (a : outParam A) (α : Sort u)
-      class C {a : A} (α : Sort u) [B a α]
-      class D {a : A} (α : Sort u) [B a α] [c : C α]
-      class E (a : A) where [c (α : Sort u) [B a α] : C α]
-      instance c {a : A} [e : E a] (α : Sort u) [B a α] : C α := e.c α
-
-      def d {a : A} [e : E a] (α : Sort u) [b : B a α] : D α := ⟨⟩
-      ```
-      The term `D α` has two instance implicit arguments. The second one has type `C α`, and TC
-      resolution produces the result `@c.{u} a e α b`.
-      Note that the `e` has type `E.{?v} a`, and `E` is universe polymorphic,
-      but the universe does not occur in the parameter `a`. We have that `?v := u` is implied by `@c.{u} a e α b`,
-      but this assignment is lost.
-  -/
-  check result
-  return some result
-
-/--
-Auxiliary function for converting a cached `AbstractMVarsResult` returned by `SynthIntance.main` into an `Expr`.
-This function tries to avoid the potentially expensive `check` at `applyCachedAbstractResult?`.
--/
-private def applyCachedAbstractResult? (type : Expr) (abstResult? : Option AbstractMVarsResult) : MetaM (Option Expr) := do
-  let some abstResult := abstResult? | return none
-  if abstResult.numMVars == 0 && abstResult.paramNames.isEmpty then
-    /-
-    Result does not instroduce new metavariables, thus we don't need to perform (again)
-    the `check` at `applyAbstractResult?`.
-    This is an optimization.
-    -/
-    unless (← assignOutParams type abstResult.expr) do
-      return none
-    return some abstResult.expr
-  else
-    applyAbstractResult? type abstResult?
-
-/-- Helper function for caching synthesized type class instances. -/
-private def cacheResult (cacheKey : SynthInstanceCacheKey) (abstResult? : Option AbstractMVarsResult) (result? : Option Expr) : MetaM Unit := do
-  match result? with
-  | none => modify fun s => { s with cache.synthInstance := s.cache.synthInstance.insert cacheKey none }
-  | some result =>
-    let some abstResult := abstResult? | return ()
-    if abstResult.numMVars == 0 && abstResult.paramNames.isEmpty then
-      -- See `applyCachedAbstractResult?` If new metavariables have **not** been introduced,
-      -- we don't need to perform extra checks again when reusing result.
-      modify fun s => { s with cache.synthInstance := s.cache.synthInstance.insert cacheKey (some { expr := result, paramNames := #[], numMVars := 0 }) }
-    else
-      modify fun s => { s with cache.synthInstance := s.cache.synthInstance.insert cacheKey (some abstResult) }
-
 def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (Option Expr) := do profileitM Exception "typeclass inference" (← getOptions) (decl := type.getAppFn.constName?.getD .anonymous) do
   let opts ← getOptions
   let maxResultSize := maxResultSize?.getD (synthInstance.maxSize.get opts)
@@ -786,20 +716,66 @@ def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (
     let localInsts ← getLocalInstances
     let type ← instantiateMVars type
     let type ← preprocess type
+    let s ← get
+    let rec assignOutParams (result : Expr) : MetaM Bool := do
+      let resultType ← inferType result
+      /- Output parameters of local instances may be marked as `syntheticOpaque` by the application-elaborator.
+         We use `withAssignableSyntheticOpaque` to make sure this kind of parameter can be assigned by the following `isDefEq`.
+         TODO: rewrite this check to avoid `withAssignableSyntheticOpaque`. -/
+      let defEq ← withDefault <| withAssignableSyntheticOpaque <| isDefEq type resultType
+      unless defEq do
+        trace[Meta.synthInstance] "{crossEmoji} result type{indentExpr resultType}\nis not definitionally equal to{indentExpr type}"
+      return defEq
     let cacheKey := { localInsts, type, synthPendingDepth := (← read).synthPendingDepth }
-    match (← get).cache.synthInstance.find? cacheKey with
-    | some abstResult? =>
-      let result? ← applyCachedAbstractResult? type abstResult?
-      trace[Meta.synthInstance] "result {result?} (cached)"
-      return result?
-    | none =>
-      let abstResult? ← withNewMCtxDepth (allowLevelAssignments := true) do
+    match s.cache.synthInstance.find? cacheKey with
+    | some result =>
+      trace[Meta.synthInstance] "result {result} (cached)"
+      if let some inst := result then
+        unless (← assignOutParams inst) do
+          return none
+      pure result
+    | none        =>
+      let result? ← withNewMCtxDepth (allowLevelAssignments := true) do
         let normType ← preprocessOutParam type
         SynthInstance.main normType maxResultSize
-      let result? ← applyAbstractResult? type abstResult?
-      trace[Meta.synthInstance] "result {result?}"
-      cacheResult cacheKey abstResult? result?
-      return result?
+      let result? ← match result? with
+        | none        => pure none
+        | some result => do
+          let (_, _, result) ← openAbstractMVarsResult result
+          trace[Meta.synthInstance] "result {result}"
+          if (← assignOutParams result) then
+            let result ← instantiateMVars result
+            /- We use `check` to propagate universe constraints implied by the `result`.
+               Recall that we use `allowLevelAssignments := true` which allows universe metavariables in the current depth to be assigned,
+               but these assignments are discarded by `withNewMCtxDepth`.
+
+               TODO: If this `check` is a performance bottleneck, we can improve performance by tracking whether
+                     a universe metavariable from previous universe levels have been assigned or not during TC resolution.
+                     We only need to perform the `check` if this kind of assignment have been performed.
+
+               The example in the issue #796 exposed this issue.
+               ```
+                structure A
+                class B (a : outParam A) (α : Sort u)
+                class C {a : A} (α : Sort u) [B a α]
+                class D {a : A} (α : Sort u) [B a α] [c : C α]
+                class E (a : A) where [c (α : Sort u) [B a α] : C α]
+                instance c {a : A} [e : E a] (α : Sort u) [B a α] : C α := e.c α
+
+                def d {a : A} [e : E a] (α : Sort u) [b : B a α] : D α := ⟨⟩
+               ```
+               The term `D α` has two instance implicit arguments. The second one has type `C α`, and TC
+               resolution produces the result `@c.{u} a e α b`.
+               Note that the `e` has type `E.{?v} a`, and `E` is universe polymorphic,
+               but the universe does not occur in the parameter `a`. We have that `?v := u` is implied by `@c.{u} a e α b`,
+               but this assignment is lost.
+            -/
+            check result
+            pure (some result)
+          else
+            pure none
+      modify fun s => { s with cache.synthInstance := s.cache.synthInstance.insert cacheKey result? }
+      pure result?
 
 /--
   Return `LOption.some r` if succeeded, `LOption.none` if it failed, and `LOption.undef` if

src/Lean/Meta/Tactic/Apply.lean

@@ -11,6 +11,34 @@ import Lean.Meta.Tactic.Util
 import Lean.PrettyPrinter
 
 namespace Lean.Meta
+/-- 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.
+-/
+inductive ApplyNewGoals where
+  | nonDependentFirst | nonDependentOnly | all
+
+/-- Configures the behaviour of the `apply` tactic. -/
+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
+
 /--
   Compute the number of expected arguments and whether the result type is of the form
   (?m ...) where ?m is an unassigned metavariable.

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean

@@ -25,12 +25,6 @@ def fromExpr? (e : Expr) : SimpM (Option Int) :=
   let some v₂ ← fromExpr? e.appArg! | return .continue
   return .done <| toExpr (op v₁ v₂)
 
-def reduceBinIntNatOp (name : Name) (op : Int → Nat → Int) (e : Expr) : SimpM DStep := do
-  unless e.isAppOfArity name 2 do return .continue
-  let some v₁ ← getIntValue? e.appFn!.appArg! | return .continue
-  let some v₂ ← getNatValue? e.appArg! | return .continue
-  return .done <| toExpr (op v₁ v₂)
-
 @[inline] def reduceBinPred (declName : Name) (arity : Nat) (op : Int → Int → Bool) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue
   let some v₁ ← fromExpr? e.appFn!.appArg! | return .continue
@@ -71,12 +65,6 @@ builtin_dsimproc [simp, seval] reduceMul ((_ * _ : Int)) := reduceBin ``HMul.hMu
 builtin_dsimproc [simp, seval] reduceSub ((_ - _ : Int)) := reduceBin ``HSub.hSub 6 (· - ·)
 builtin_dsimproc [simp, seval] reduceDiv ((_ / _ : Int)) := reduceBin ``HDiv.hDiv 6 (· / ·)
 builtin_dsimproc [simp, seval] reduceMod ((_ % _ : Int)) := reduceBin ``HMod.hMod 6 (· % ·)
-builtin_dsimproc [simp, seval] reduceTDiv (div  _ _) := reduceBin ``Int.div 2 Int.div
-builtin_dsimproc [simp, seval] reduceTMod (mod  _ _) := reduceBin ``Int.mod 2 Int.mod
-builtin_dsimproc [simp, seval] reduceFDiv (fdiv _ _) := reduceBin ``Int.fdiv 2 Int.fdiv
-builtin_dsimproc [simp, seval] reduceFMod (fmod _ _) := reduceBin ``Int.fmod 2 Int.fmod
-builtin_dsimproc [simp, seval] reduceBdiv (bdiv _ _) := reduceBinIntNatOp ``bdiv bdiv
-builtin_dsimproc [simp, seval] reduceBmod (bmod _ _) := reduceBinIntNatOp ``bmod bmod
 
 builtin_dsimproc [simp, seval] reducePow ((_ : Int) ^ (_ : Nat)) := fun e => do
   let_expr HPow.hPow _ _ _ _ a b ← e | return .continue

src/Lean/Meta/Tactic/Simp/Main.lean

@@ -430,10 +430,7 @@ private def doNotVisit (pred : Expr → Bool) (declName : Name) : DSimproc := fu
     if (← readThe Simp.Context).isDeclToUnfold declName then
       return .continue e
     else
-      -- Users may have added a `[simp]` rfl theorem for the literal
-      match (← (← getMethods).dpost e) with
-      | .continue none => return .done e
-      | r => return r
+      return .done e
   else
     return .continue e
 

src/Lean/Meta/Tactic/Simp/SimpTheorems.lean

@@ -175,7 +175,7 @@ def ppOrigin [Monad m] [MonadEnv m] [MonadError m] : Origin → m MessageData
   | .stx _ ref => return ref
   | .other n => return n
 
-def ppSimpTheorem [Monad m] [MonadEnv m] [MonadError m] (s : SimpTheorem) : m MessageData := do
+def ppSimpTheorem [Monad m] [MonadLiftT IO m] [MonadEnv m] [MonadError m] (s : SimpTheorem) : m MessageData := do
   let perm := if s.perm then ":perm" else ""
   let name ← ppOrigin s.origin
   let prio := m!":{s.priority}"

src/Lean/Meta/Tactic/Simp/Types.lean

@@ -106,21 +106,8 @@ structure Context where
 def Context.isDeclToUnfold (ctx : Context) (declName : Name) : Bool :=
   ctx.simpTheorems.isDeclToUnfold declName
 
-structure UsedSimps where
-  -- We should use `PHashMap` because we backtrack the contents of `UsedSimps`
-  -- The natural number tracks the insertion order
-  map  : PHashMap Origin Nat := {}
-  size : Nat := 0
-  deriving Inhabited
-
-def UsedSimps.insert (s : UsedSimps) (thmId : Origin) : UsedSimps :=
-  if s.map.contains thmId then
-    s
-  else match s with
-    | { map, size } => { map := map.insert thmId size, size := size + 1 }
-
-def UsedSimps.toArray (s : UsedSimps) : Array Origin :=
-  s.map.toArray.qsort (·.2 < ·.2) |>.map (·.1)
+-- We should use `PHashMap` because we backtrack the contents of `UsedSimps`
+abbrev UsedSimps := PHashMap Origin Nat
 
 structure Diagnostics where
   /-- Number of times each simp theorem has been used/applied. -/
@@ -380,7 +367,9 @@ def recordSimpTheorem (thmId : Origin) : SimpM Unit := do
       else
         pure thmId
     | _ => pure thmId
-  modify fun s => { s with usedTheorems := s.usedTheorems.insert thmId }
+  modify fun s => if s.usedTheorems.contains thmId then s else
+    let n := s.usedTheorems.size
+    { s with usedTheorems := s.usedTheorems.insert thmId n }
 
 def recordCongrTheorem (declName : Name) : SimpM Unit := do
   modifyDiag fun s =>

src/Lean/Meta/Transform.lean

@@ -21,7 +21,7 @@ inductive TransformStep where
   For `pre`, this means visiting the children of the expression.
   For `post`, this is equivalent to returning `done`. -/
   | continue (e? : Option Expr := none)
-  deriving Inhabited, Repr
+  deriving Inhabited
 
 namespace Core
 
@@ -81,7 +81,7 @@ namespace Meta
   `.const f` is not visited again. Put differently: every `.const f` is visited once, with its
   arguments if present, on its own otherwise.
  -/
-partial def transform {m} [Monad m] [MonadLiftT MetaM m] [MonadControlT MetaM m]
+partial def transform {m} [Monad m] [MonadLiftT MetaM m] [MonadControlT MetaM m] [MonadTrace m] [MonadRef m] [MonadOptions m] [AddMessageContext m]
     (input : Expr)
     (pre   : Expr → m TransformStep := fun _ => return .continue)
     (post  : Expr → m TransformStep := fun e => return .done e)

src/Lean/MetavarContext.lean

@@ -1274,25 +1274,13 @@ partial def revert (xs : Array Expr) (mvarId : MVarId) : M (Expr × Array Expr)
   let e ← elimMVarDeps xs e
   pure (e.abstractRange i xs)
 
-private def mkLambda' (x : Name) (bi : BinderInfo) (t : Expr) (b : Expr) (etaReduce : Bool) : Expr :=
-  if etaReduce then
-    match b with
-    | .app f (.bvar 0) =>
-      if !f.hasLooseBVar 0 then
-        f.lowerLooseBVars 1 1
-      else
-        mkLambda x bi t b
-    | _ => mkLambda x bi t b
-  else
-    mkLambda x bi t b
-
 /--
   Similar to `LocalContext.mkBinding`, but handles metavariables correctly.
   If `usedOnly == true` then `forall` and `lambda` expressions are created only for used variables.
   If `usedLetOnly == true` then `let` expressions are created only for used (let-) variables. -/
-@[specialize] def mkBinding (isLambda : Bool) (lctx : LocalContext) (xs : Array Expr) (e : Expr) (usedOnly : Bool) (usedLetOnly : Bool) (etaReduce : Bool) : M Expr := do
+@[specialize] def mkBinding (isLambda : Bool) (lctx : LocalContext) (xs : Array Expr) (e : Expr) (usedOnly : Bool) (usedLetOnly : Bool) : M (Expr × Nat) := do
   let e ← abstractRange xs xs.size e
-  xs.size.foldRevM (init := e) fun i e => do
+  xs.size.foldRevM (init := (e, 0)) fun i (e, num) => do
       let x := xs[i]!
       if x.isFVar then
         match lctx.getFVar! x with
@@ -1301,27 +1289,27 @@ private def mkLambda' (x : Name) (bi : BinderInfo) (t : Expr) (b : Expr) (etaRed
             let type := type.headBeta;
             let type ← abstractRange xs i type
             if isLambda then
-              return mkLambda' n bi type e etaReduce
+              return (Lean.mkLambda n bi type e, num + 1)
             else
-              return Lean.mkForall n bi type e
+              return (Lean.mkForall n bi type e, num + 1)
           else
-            return e.lowerLooseBVars 1 1
+            return (e.lowerLooseBVars 1 1, num)
         | LocalDecl.ldecl _ _ n type value nonDep _ =>
           if !usedLetOnly || e.hasLooseBVar 0 then
             let type  ← abstractRange xs i type
             let value ← abstractRange xs i value
-            return mkLet n type value e nonDep
+            return (mkLet n type value e nonDep, num + 1)
           else
-            return e.lowerLooseBVars 1 1
+            return (e.lowerLooseBVars 1 1, num)
       else
         let mvarDecl := (← get).mctx.getDecl x.mvarId!
         let type := mvarDecl.type.headBeta
         let type ← abstractRange xs i type
         let id ← if mvarDecl.userName.isAnonymous then mkFreshBinderName else pure mvarDecl.userName
         if isLambda then
-          return mkLambda' id (← read).binderInfoForMVars type e etaReduce
+          return (Lean.mkLambda id (← read).binderInfoForMVars type e, num + 1)
         else
-          return Lean.mkForall id (← read).binderInfoForMVars type e
+          return (Lean.mkForall id (← read).binderInfoForMVars type e, num + 1)
 
 end MkBinding
 
@@ -1337,15 +1325,15 @@ def elimMVarDeps (xs : Array Expr) (e : Expr) (preserveOrder : Bool) : MkBinding
 def revert (xs : Array Expr) (mvarId : MVarId) (preserveOrder : Bool) : MkBindingM (Expr × Array Expr) := fun ctx =>
   MkBinding.revert xs mvarId { preserveOrder, mainModule := ctx.mainModule }
 
-def mkBinding (isLambda : Bool) (xs : Array Expr) (e : Expr) (usedOnly : Bool := false) (usedLetOnly : Bool := true) (etaReduce := false) (binderInfoForMVars := BinderInfo.implicit) : MkBindingM Expr := fun ctx =>
+def mkBinding (isLambda : Bool) (xs : Array Expr) (e : Expr) (usedOnly : Bool := false) (usedLetOnly : Bool := true) (binderInfoForMVars := BinderInfo.implicit) : MkBindingM (Expr × Nat) := fun ctx =>
   let mvarIdsToAbstract := xs.foldl (init := {}) fun s x => if x.isMVar then s.insert x.mvarId! else s
-  MkBinding.mkBinding isLambda ctx.lctx xs e usedOnly usedLetOnly etaReduce { preserveOrder := false, binderInfoForMVars, mvarIdsToAbstract, mainModule := ctx.mainModule }
+  MkBinding.mkBinding isLambda ctx.lctx xs e usedOnly usedLetOnly { preserveOrder := false, binderInfoForMVars, mvarIdsToAbstract, mainModule := ctx.mainModule }
 
-@[inline] def mkLambda (xs : Array Expr) (e : Expr) (usedOnly : Bool := false) (usedLetOnly : Bool := true) (etaReduce := false) (binderInfoForMVars := BinderInfo.implicit) : MkBindingM Expr :=
-  return ← mkBinding (isLambda := true) xs e usedOnly usedLetOnly etaReduce binderInfoForMVars
+@[inline] def mkLambda (xs : Array Expr) (e : Expr) (usedOnly : Bool := false) (usedLetOnly : Bool := true) (binderInfoForMVars := BinderInfo.implicit) : MkBindingM Expr :=
+  return (← mkBinding (isLambda := true) xs e usedOnly usedLetOnly binderInfoForMVars).1
 
 @[inline] def mkForall (xs : Array Expr) (e : Expr) (usedOnly : Bool := false) (usedLetOnly : Bool := true) (binderInfoForMVars := BinderInfo.implicit) : MkBindingM Expr :=
-  return ← mkBinding (isLambda := false) xs e usedOnly usedLetOnly false binderInfoForMVars
+  return (← mkBinding (isLambda := false) xs e usedOnly usedLetOnly binderInfoForMVars).1
 
 @[inline] def abstractRange (e : Expr) (n : Nat) (xs : Array Expr) : MkBindingM Expr := fun ctx =>
   MkBinding.abstractRange xs n e { preserveOrder := false, mainModule := ctx.mainModule }

src/Lean/Modifiers.lean

@@ -10,9 +10,11 @@ namespace Lean
 
 builtin_initialize protectedExt : TagDeclarationExtension ← mkTagDeclarationExtension
 
+@[export lean_add_protected]
 def addProtected (env : Environment) (n : Name) : Environment :=
   protectedExt.tag env n
 
+@[export lean_is_protected]
 def isProtected (env : Environment) (n : Name) : Bool :=
   protectedExt.isTagged env n
 

src/Lean/Parser.lean

@@ -12,7 +12,6 @@ import Lean.Parser.Command
 import Lean.Parser.Module
 import Lean.Parser.Syntax
 import Lean.Parser.Do
-import Lean.Parser.Tactic.Doc
 
 namespace Lean
 namespace Parser

src/Lean/Parser/Attr.lean

@@ -50,24 +50,6 @@ def externEntry := leading_parser
 @[builtin_attr_parser] def extern     := leading_parser
   nonReservedSymbol "extern" >> optional (ppSpace >> numLit) >> many (ppSpace >> externEntry)
 
-/--
-Declare this tactic to be an alias or alternative form of an existing tactic.
-
-This has the following effects:
- * The alias relationship is saved
- * The docstring is taken from the original tactic, if present
--/
-@[builtin_attr_parser] def «tactic_alt» := leading_parser
-  "tactic_alt" >> ppSpace >> ident
-
-/--
-Add one or more tags to a tactic.
-
-Tags should be applied to the canonical names for tactics.
--/
-@[builtin_attr_parser] def «tactic_tag» := leading_parser
-  "tactic_tag" >> many1 (ppSpace >> ident)
-
 end Attr
 
 end Lean.Parser

src/Lean/Parser/Command.lean

@@ -447,11 +447,6 @@ structure Pair (α : Type u) (β : Type v) : Type (max u v) where
   "#print " >> nonReservedSymbol "axioms " >> ident
 @[builtin_command_parser] def printEqns      := leading_parser
   "#print " >> (nonReservedSymbol "equations " <|> nonReservedSymbol "eqns ") >> ident
-/--
-Displays all available tactic tags, with documentation.
--/
-@[builtin_command_parser] def printTacTags   := leading_parser
-  "#print " >> nonReservedSymbol "tactic " >> nonReservedSymbol "tags"
 @[builtin_command_parser] def «init_quot»    := leading_parser
   "init_quot"
 def optionValue := nonReservedSymbol "true" <|> nonReservedSymbol "false" <|> strLit <|> numLit
@@ -674,26 +669,6 @@ Documentation can only be added to declarations in the same module.
 @[builtin_command_parser] def addDocString := leading_parser
   docComment >> "add_decl_doc " >> ident
 
-/--
-Register a tactic tag, saving its user-facing name and docstring.
-
-Tactic tags can be used by documentation generation tools to classify related tactics.
--/
-@[builtin_command_parser] def «register_tactic_tag» := leading_parser
-  optional (docComment >> ppLine) >>
-  "register_tactic_tag " >> ident >> strLit
-
-/--
-Add more documentation as an extension of the documentation for a given tactic.
-
-The extended documentation is placed in the command's docstring. It is shown as part of a bulleted
-list, so it should be brief.
--/
-@[builtin_command_parser] def «tactic_extension» := leading_parser
-  optional (docComment >> ppLine) >>
-  "tactic_extension " >> ident
-
-
 /--
   This is an auxiliary command for generation constructor injectivity theorems for
   inductive types defined at `Prelude.lean`.

src/Lean/Parser/Tactic.lean

@@ -5,7 +5,6 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
 import Lean.Parser.Term
-import Lean.Parser.Tactic.Doc
 
 namespace Lean
 namespace Parser

src/Lean/Parser/Tactic/Doc.lean

@@ -1,290 +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.Attributes
-import Lean.DocString.Extension
-import Lean.Elab.InfoTree.Main
-import Lean.Parser.Attr
-import Lean.Parser.Extension
-
-set_option linter.missingDocs true
-
-namespace Lean.Parser.Tactic.Doc
-
-open Lean.Parser (registerParserAttributeHook)
-open Lean.Parser.Attr
-
-/-- Check whether a name is a tactic syntax kind -/
-def isTactic (env : Environment) (kind : Name) : Bool := Id.run do
-  let some tactics := (Lean.Parser.parserExtension.getState env).categories.find? `tactic
-    | return false
-  for (tac, _) in tactics.kinds do
-    if kind == tac then return true
-  return false
-
-/--
-Stores a collection of *tactic alternatives*, to track which new syntax rules represent new forms of
-existing tactics.
--/
-builtin_initialize tacticAlternativeExt
-    : PersistentEnvExtension (Name × Name) (Name × Name) (NameMap Name) ←
-  registerPersistentEnvExtension {
-    mkInitial := pure {},
-    addImportedFn := fun _ => pure {},
-    addEntryFn := fun as (src, tgt) => as.insert src tgt,
-    exportEntriesFn := fun es =>
-      es.fold (fun a src tgt => a.push (src, tgt)) #[] |>.qsort (Name.quickLt ·.1 ·.1)
-  }
-
-/--
-If `tac` is registered as the alternative form of another tactic, then return the canonical name for
-it.
--/
-def alternativeOfTactic (env : Environment) (tac : Name) : Option Name :=
-  match env.getModuleIdxFor? tac with
-  | some modIdx =>
-    match (tacticAlternativeExt.getModuleEntries env modIdx).binSearch (tac, .anonymous) (Name.quickLt ·.1 ·.1) with
-    | some (_, val) => some val
-    | none => none
-  | none => tacticAlternativeExt.getState env |>.find? tac
-
-/--
-Find all alternatives for a given canonical tactic name.
--/
-def aliases [Monad m] [MonadEnv m] (tac : Name) : m NameSet := do
-  let env ← getEnv
-  let mut found := {}
-  for (src, tgt) in tacticAlternativeExt.getState env do
-    if tgt == tac then found := found.insert src
-  for arr in tacticAlternativeExt.toEnvExtension.getState env |>.importedEntries do
-    for (src, tgt) in arr do
-      if tgt == tac then found := found.insert src
-  pure found
-
-builtin_initialize
-  let name := `tactic_alt
-  registerBuiltinAttribute {
-    name := name,
-    ref := by exact decl_name%,
-    add := fun decl stx kind => do
-      unless kind == AttributeKind.global do throwError "invalid attribute '{name}', must be global"
-      unless ((← getEnv).getModuleIdxFor? decl).isNone do
-        throwError "invalid attribute '{name}', declaration is in an imported module"
-      let `(«tactic_alt»|tactic_alt $tgt) := stx
-        | throwError "invalid syntax for '{name}' attribute"
-
-      let tgtName ← Lean.Elab.realizeGlobalConstNoOverloadWithInfo tgt
-
-      if !(isTactic (← getEnv) tgtName) then throwErrorAt tgt "'{tgtName}' is not a tactic"
-      -- If this condition is true, then we're in an `attribute` command and can validate here.
-      if (← getEnv).find? decl |>.isSome then
-        if !(isTactic (← getEnv) decl) then throwError "'{decl}' is not a tactic"
-
-      if let some tgt' := alternativeOfTactic (← getEnv) tgtName then
-        throwError "'{tgtName}' is itself an alternative for '{tgt'}'"
-      modifyEnv fun env => tacticAlternativeExt.addEntry env (decl, tgtName)
-      if (← findSimpleDocString? (← getEnv) decl).isSome then
-        logWarningAt stx m!"Docstring for '{decl}' will be ignored because it is an alternative"
-
-    descr :=
-      "Register a tactic parser as an alternative form of an existing tactic, so they " ++
-      "can be grouped together in documentation.",
-    -- This runs prior to elaboration because it allows a check for whether the decl is present
-    -- in the environment to determine whether we can see if it's a tactic name. This is useful
-    -- when the attribute is applied after definition, using an `attribute` command (error checking
-    -- for the `@[tactic_alt TAC]` syntax is performed by the parser attribute hook). If this
-    -- attribute ran later, then the decl would already be present.
-    applicationTime := .beforeElaboration
-  }
-
-
-/--
-The known tactic tags that allow tactics to be grouped by purpose.
--/
-builtin_initialize knownTacticTagExt
-    : PersistentEnvExtension
-        (Name × String × Option String)
-        (Name × String × Option String)
-        (NameMap (String × Option String)) ←
-  registerPersistentEnvExtension {
-    mkInitial := pure {},
-    addImportedFn := fun _ => pure {},
-    addEntryFn := fun as (src, tgt) => as.insert src tgt,
-    exportEntriesFn := fun es =>
-      es.fold (fun a src tgt => a.push (src, tgt)) #[] |>.qsort (Name.quickLt ·.1 ·.1)
-  }
-
-/--
-Get the user-facing name and docstring for a tactic tag.
--/
-def tagInfo [Monad m] [MonadEnv m] (tag : Name) : m (Option (String × Option String)) := do
-  let env ← getEnv
-  match env.getModuleIdxFor? tag with
-  | some modIdx =>
-    match (knownTacticTagExt.getModuleEntries env modIdx).binSearch (tag, default) (Name.quickLt ·.1 ·.1) with
-    | some (_, val) => pure (some val)
-    | none => pure none
-  | none => pure (knownTacticTagExt.getState env |>.find? tag)
-
-/-- Enumerate the tactic tags that are available -/
-def allTags [Monad m] [MonadEnv m] : m (List Name) := do
-  let env ← getEnv
-  let mut found : NameSet := {}
-  for (tag, _) in knownTacticTagExt.getState env do
-    found := found.insert tag
-  for arr in knownTacticTagExt.toEnvExtension.getState env |>.importedEntries do
-    for (tag, _) in arr do
-      found := found.insert tag
-  pure (found.toArray.qsort (·.toString < ·.toString) |>.toList)
-
-/-- Enumerate the tactic tags that are available, with their user-facing name and docstring -/
-def allTagsWithInfo [Monad m] [MonadEnv m] : m (List (Name × String × Option String)) := do
-  let env ← getEnv
-  let mut found : NameMap (String × Option String) := {}
-  for (tag, info) in knownTacticTagExt.getState env do
-    found := found.insert tag info
-  for arr in knownTacticTagExt.toEnvExtension.getState env |>.importedEntries do
-    for (tag, info) in arr do
-      found := found.insert tag info
-  let arr := found.fold (init := #[]) (fun arr k v => arr.push (k, v))
-  pure (arr.qsort (·.1.toString < ·.1.toString) |>.toList)
-
-/--
-The mapping between tags and tactics. Tags may be applied in any module, not just the defining
-module for the tactic.
-
-Because this is expected to be augmented regularly, but queried rarely (only when generating
-documentation indices), it is just stored as flat unsorted arrays of pairs. Before it is used for
-some other purpose, consider a new representation.
-
-The first projection in each pair is the tactic name, and the second is the tag name.
--/
-builtin_initialize tacticTagExt
-    : PersistentEnvExtension (Name × Name) (Name × Name) (NameMap NameSet) ←
-  registerPersistentEnvExtension {
-    mkInitial := pure {},
-    addImportedFn := fun _ => pure {},
-    addEntryFn := fun tags (decl, newTag) => tags.insert decl (tags.findD decl {} |>.insert newTag)
-    exportEntriesFn := fun tags => Id.run do
-      let mut exported := #[]
-      for (decl, dTags) in tags do
-        for t in dTags do
-          exported := exported.push (decl, t)
-      exported
-  }
-
-builtin_initialize
-  let name := `tactic_tag
-  registerBuiltinAttribute {
-    name := name,
-    ref := by exact decl_name%,
-    add := fun decl stx kind => do
-      unless kind == AttributeKind.global do throwError "invalid attribute '{name}', must be global"
-      let `(«tactic_tag»|tactic_tag $tags*) := stx
-        | throwError "invalid '{name}' attribute"
-      if (← getEnv).find? decl |>.isSome then
-        if !(isTactic (← getEnv) decl) then
-          throwErrorAt stx "'{decl}' is not a tactic"
-
-      if let some tgt' := alternativeOfTactic (← getEnv) decl then
-        throwErrorAt stx "'{decl}' is an alternative form of '{tgt'}'"
-
-      for t in tags do
-        let tagName := t.getId
-        if let some _ ← tagInfo tagName then
-          modifyEnv (tacticTagExt.addEntry · (decl, tagName))
-        else
-          let all ← allTags
-          let extra : MessageData :=
-              let count := all.length
-              let name := (m!"'{·}'")
-              let suggestions :=
-                if count == 0 then m!"(no tags defined)"
-                else if count == 1 then
-                  MessageData.joinSep (all.map name) ", "
-                else if count < 10 then
-                  m!"one of " ++ MessageData.joinSep (all.map name) ", "
-                else
-                  m!"one of " ++
-                  MessageData.joinSep (all.take 10 |>.map name) ", " ++ ", ..."
-              m!"(expected {suggestions})"
-
-          throwErrorAt t (m!"unknown tag '{tagName}' " ++ extra)
-    descr := "Register a tactic parser as an alternative of an existing tactic, so they can be " ++
-      "grouped together in documentation.",
-    -- This runs prior to elaboration because it allows a check for whether the decl is present
-    -- in the environment to determine whether we can see if it's a tactic name. This is useful
-    -- when the attribute is applied after definition, using an `attribute` command (error checking
-    -- for the `@[tactic_tag ...]` syntax is performed by the parser attribute hook). If this
-    -- attribute ran later, then the decl would already be present.
-    applicationTime := .beforeElaboration
-  }
-
-/--
-Extensions to tactic documentation.
-
-This provides a structured way to indicate that an extensible tactic has been extended (for
-instance, new cases tried by `trivial`).
--/
-builtin_initialize tacticDocExtExt
-    : PersistentEnvExtension (Name × Array String) (Name × String) (NameMap (Array String)) ←
-  registerPersistentEnvExtension {
-    mkInitial := pure {},
-    addImportedFn := fun _ => pure {},
-    addEntryFn := fun es (x, ext) => es.insert x (es.findD x #[] |>.push ext),
-    exportEntriesFn := fun es =>
-      es.fold (fun a src tgt => a.push (src, tgt)) #[] |>.qsort (Name.quickLt ·.1 ·.1)
-  }
-
-/-- Gets the extensions declared for the documentation for the given canonical tactic name -/
-def getTacticExtensions (env : Environment) (tactic : Name) : Array String := Id.run do
-  let mut extensions := #[]
-  -- Extensions may be declared in any module, so they must all be searched
-  for modArr in tacticDocExtExt.toEnvExtension.getState env |>.importedEntries do
-    if let some (_, strs) := modArr.binSearch (tactic, #[]) (Name.quickLt ·.1 ·.1) then
-      extensions := extensions ++ strs
-  if let some strs := tacticDocExtExt.getState env |>.find? tactic then
-    extensions := extensions ++ strs
-  pure extensions
-
-/-- Gets the rendered extensions for the given canonical tactic name -/
-def getTacticExtensionString (env : Environment) (tactic : Name) : String := Id.run do
-  let exts := getTacticExtensions env tactic
-  if exts.size == 0 then ""
-  else "\n\nExtensions:\n\n" ++ String.join (exts.toList.map bullet) |>.trimRight
-where
-  indentLine (str: String) : String :=
-    (if str.all (·.isWhitespace) then str else "   " ++ str) ++ "\n"
-  bullet (str : String) : String :=
-    let lines := str.splitOn "\n"
-    match lines with
-    | [] => ""
-    | [l] => " * " ++ l ++ "\n\n"
-    | l::ls => " * " ++ l ++ "\n" ++ String.join (ls.map indentLine) ++ "\n\n"
-
-
--- Note: this error handler doesn't prevent all cases of non-tactics being added to the data
--- structure. But the module will throw errors during elaboration, and there doesn't seem to be
--- another way to implement this, because the category parser extension attribute runs *after* the
--- attributes specified before a `syntax` command.
-/--
-Validates that a tactic alternative is actually a tactic and that syntax tagged as tactics are
-tactics.
--/
-def tacticDocsOnTactics : ParserAttributeHook where
-  postAdd (catName declName : Name) (_builtIn : Bool) := do
-    if catName == `tactic then
-      return
-    if alternativeOfTactic (← getEnv) declName |>.isSome then
-      throwError m!"'{declName}' is not a tactic"
-    -- It's sufficient to look in the state (and not the imported entries) because this validation
-    -- only needs to check tags added in the current module
-    if let some tags := tacticTagExt.getState (← getEnv) |>.find? declName then
-      if !tags.isEmpty then
-        throwError m!"'{declName}' is not a tactic"
-
-builtin_initialize
-  registerParserAttributeHook tacticDocsOnTactics

src/Lean/ReducibilityAttrs.lean

@@ -165,11 +165,11 @@ def getReducibilityStatus [Monad m] [MonadEnv m] (declName : Name) : m Reducibil
   return getReducibilityStatusCore (← getEnv) declName
 
 /-- Set the reducibility attribute for the given declaration. -/
-def setReducibilityStatus [MonadEnv m] (declName : Name) (s : ReducibilityStatus) : m Unit :=
+def setReducibilityStatus [Monad m] [MonadEnv m] (declName : Name) (s : ReducibilityStatus) : m Unit := do
   modifyEnv fun env => setReducibilityStatusCore env declName s .global .anonymous
 
 /-- Set the given declaration as `[reducible]` -/
-def setReducibleAttribute [MonadEnv m] (declName : Name) : m Unit :=
+def setReducibleAttribute [Monad m] [MonadEnv m] (declName : Name) : m Unit := do
   setReducibilityStatus declName ReducibilityStatus.reducible
 
 /-- Return `true` if the given declaration has been marked as `[reducible]`. -/
@@ -185,7 +185,7 @@ def isIrreducible [Monad m] [MonadEnv m] (declName : Name) : m Bool := do
   | _ => return false
 
 /-- Set the given declaration as `[irreducible]` -/
-def setIrreducibleAttribute [MonadEnv m] (declName : Name) : m Unit :=
+def setIrreducibleAttribute [Monad m] [MonadEnv m] (declName : Name) : m Unit := do
   setReducibilityStatus declName ReducibilityStatus.irreducible
 
 

src/Lean/ResolveName.lean

@@ -187,17 +187,10 @@ def resolveGlobalName (env : Environment) (ns : Name) (openDecls : List OpenDecl
 
 /-! # Namespace resolution -/
 
-def resolveNamespaceUsingScope? (env : Environment) (n : Name) (ns : Name) : Option Name :=
-  match ns with
-  | .str p _ =>
-    if env.isNamespace (ns ++ n) then
-      some (ns ++ n)
-    else
-      resolveNamespaceUsingScope? env n p
-  | .anonymous =>
-    let n := n.replacePrefix rootNamespace .anonymous
-    if env.isNamespace n then some n else none
-  | _ => unreachable!
+def resolveNamespaceUsingScope? (env : Environment) (n : Name) : Name → Option Name
+  | .anonymous    => if env.isNamespace n then some n else none
+  | ns@(.str p _) => if env.isNamespace (ns ++ n) then some (ns ++ n) else resolveNamespaceUsingScope? env n p
+  | _             => unreachable!
 
 def resolveNamespaceUsingOpenDecls (env : Environment) (n : Name) : List OpenDecl → List Name
   | [] => []
@@ -314,7 +307,7 @@ def ensureNoOverload [Monad m] [MonadError m] (n : Name) (cs : List Name) : m Na
 def resolveGlobalConstNoOverloadCore [Monad m] [MonadResolveName m] [MonadEnv m] [MonadError m] (n : Name) : m Name := do
   ensureNoOverload n (← resolveGlobalConstCore n)
 
-def preprocessSyntaxAndResolve [Monad m] [MonadEnv m] [MonadError m] (stx : Syntax) (k : Name → m (List Name)) : m (List Name) := do
+def preprocessSyntaxAndResolve [Monad m] [MonadResolveName m] [MonadEnv m] [MonadError m] (stx : Syntax) (k : Name → m (List Name)) : m (List Name) := do
   match stx with
   | .ident _ _ n pre => do
     let pre := pre.filterMap fun

src/Lean/Server/FileWorker/RequestHandling.lean

@@ -10,8 +10,6 @@ import Lean.DeclarationRange
 import Lean.Data.Json
 import Lean.Data.Lsp
 
-import Lean.Parser.Tactic.Doc
-
 import Lean.Server.FileWorker.Utils
 import Lean.Server.Requests
 import Lean.Server.Completion
@@ -26,8 +24,6 @@ open Lsp
 open RequestM
 open Snapshots
 
-open Lean.Parser.Tactic.Doc (alternativeOfTactic getTacticExtensionString)
-
 def handleCompletion (p : CompletionParams)
     : RequestM (RequestTask CompletionList) := do
   let doc ← readDoc
@@ -89,8 +85,7 @@ def handleHover (p : HoverParams)
       let stxDoc? ← match stack? with
         | some stack => stack.findSomeM? fun (stx, _) => do
           let .node _ kind _ := stx | pure none
-          let docStr ← findDocString? snap.env kind
-          return docStr.map (·, stx.getRange?.get!)
+          return (← findDocString? snap.env kind).map (·, stx.getRange?.get!)
         | none => pure none
 
       -- now try info tree

src/Lean/Server/InfoUtils.lean

@@ -5,14 +5,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Wojciech Nawrocki
 -/
 prelude
-import Lean.DocString
 import Lean.PrettyPrinter
-import Lean.Parser.Tactic.Doc
 
 namespace Lean.Elab
 
-open Lean.Parser.Tactic.Doc (alternativeOfTactic getTacticExtensionString)
-
 /-- Elaborator information with elaborator context.
 
 It can be thought of as a "thunked" elaboration computation that allows us
@@ -248,7 +244,7 @@ def Info.docString? (i : Info) : MetaM (Option String) := do
   match i with
   | .ofTermInfo ti =>
     if let some n := ti.expr.constName? then
-      return (← findDocString? env n)
+      return ← findDocString? env n
   | .ofFieldInfo fi => return ← findDocString? env fi.projName
   | .ofOptionInfo oi =>
     if let some doc ← findDocString? env oi.declName then
@@ -262,7 +258,6 @@ def Info.docString? (i : Info) : MetaM (Option String) := do
     return ← findDocString? env ei.stx.getKind <||> findDocString? env ei.elaborator
   return none
 
-
 /-- Construct a hover popup, if any, from an info node in a context.-/
 def Info.fmtHover? (ci : ContextInfo) (i : Info) : IO (Option FormatWithInfos) := do
   ci.runMetaM i.lctx do

src/Lean/Util/ForEachExprWhere.lean

@@ -16,6 +16,8 @@ if the number of subterms satisfying `p` is a small subset of the set of subterm
 If `p` holds for most subterms, then it is more efficient to use `forEach f e`.
 -/
 
+variable {ω : Type} {m : Type → Type} [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m]
+
 namespace ForEachExprWhere
 abbrev cacheSize : USize := 8192 - 1
 
@@ -35,9 +37,7 @@ unsafe def initCache : State := {
   checked := {}
 }
 
-abbrev ForEachM {ω : Type} (m : Type → Type) [STWorld ω m] := StateRefT' ω State m
-
-variable {ω : Type} {m : Type → Type} [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m]
+abbrev ForEachM {ω : Type} (m : Type → Type) [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m] := StateRefT' ω State m
 
 unsafe def visited (e : Expr) : ForEachM m Bool := do
   let s ← get

src/Leanc.lean

@@ -8,15 +8,10 @@ import Lean.Compiler.FFI
 open Lean.Compiler.FFI
 
 def main (args : List String) : IO UInt32 := do
-  let root ← match (← IO.getEnv "LEAN_SYSROOT") with
-    | some root => pure <| System.FilePath.mk root
-    | none      => pure <| (← IO.appDir).parent.get!
-  let mut cc := "@LEANC_CC@".replace "ROOT" root.toString
-
   if args.isEmpty then
-    IO.println s!"Lean C compiler
+    IO.println "Lean C compiler
 
-A simple wrapper around a C compiler. Defaults to `{cc}`,
+A simple wrapper around a C compiler. Defaults to `@LEANC_CC@`,
 which can be overridden with the environment variable `LEAN_CC`. All parameters are passed
 as-is to the wrapped compiler.
 
@@ -25,6 +20,11 @@ Interesting options:
 * `--print-ldflags`: print C compiler flags necessary for statically linking against the Lean library and exit"
     return 1
 
+  let root ← match (← IO.getEnv "LEAN_SYSROOT") with
+    | some root => pure <| System.FilePath.mk root
+    | none      => pure <| (← IO.appDir).parent.get!
+  let rootify s := s.replace "ROOT" root.toString
+
   -- It is difficult to identify the correct minor version here, leading to linking warnings like:
   -- `ld64.lld: warning: /usr/lib/system/libsystem_kernel.dylib has version 13.5.0, which is newer than target minimum of 13.0.0`
   -- In order to suppress these we set the MACOSX_DEPLOYMENT_TARGET variable into the far future.
@@ -38,27 +38,29 @@ Interesting options:
 
   -- We assume that the CMake variables do not contain escaped spaces
   let cflags := getCFlags root
-  let mut cflagsInternal := getInternalCFlags root
-  let mut ldflagsInternal := getInternalLinkerFlags root
+  let mut cflagsInternal := "@LEANC_INTERNAL_FLAGS@".trim.splitOn
+  let mut ldflagsInternal := "@LEANC_INTERNAL_LINKER_FLAGS@".trim.splitOn
   let ldflags := getLinkerFlags root linkStatic
 
   for arg in args do
     match arg with
     | "--print-cflags" =>
-      IO.println <| " ".intercalate cflags.toList
+      IO.println <| " ".intercalate (cflags.map rootify |>.toList)
       return 0
     | "--print-ldflags" =>
-      IO.println <| " ".intercalate (cflags ++ ldflags).toList
+      IO.println <| " ".intercalate ((cflags ++ ldflags).map rootify |>.toList)
       return 0
     | _ => pure ()
 
+  let mut cc := "@LEANC_CC@"
   if let some cc' ← IO.getEnv "LEAN_CC" then
     cc := cc'
     -- these are intended for the bundled compiler only
-    cflagsInternal := #[]
-    ldflagsInternal := #[]
+    cflagsInternal := []
+    ldflagsInternal := []
+  cc := rootify cc
   let args := cflags ++ cflagsInternal ++ args ++ ldflagsInternal ++ ldflags ++ ["-Wno-unused-command-line-argument"]
-  let args := args.filter (!·.isEmpty)
+  let args := args.filter (!·.isEmpty) |>.map rootify
   if args.contains "-v" then
     IO.eprintln s!"{cc} {" ".intercalate args.toList}"
   let child ← IO.Process.spawn { cmd := cc, args, env }

src/Std.lean

@@ -1,5 +0,0 @@
-/-
-Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sebastian Ullrich
--/

src/include/lean/lean.h

@@ -990,10 +990,7 @@ static inline size_t lean_string_capacity(lean_object * o) { return lean_to_stri
 static inline size_t lean_string_byte_size(lean_object * o) { return sizeof(lean_string_object) + lean_string_capacity(o); }
 /* instance : inhabited char := ⟨'A'⟩ */
 static inline uint32_t lean_char_default_value() { return 'A'; }
-LEAN_EXPORT lean_obj_res lean_mk_string_unchecked(char const * s, size_t sz, size_t len);
 LEAN_EXPORT lean_obj_res lean_mk_string_from_bytes(char const * s, size_t sz);
-LEAN_EXPORT lean_obj_res lean_mk_string_from_bytes_unchecked(char const * s, size_t sz);
-LEAN_EXPORT lean_obj_res lean_mk_ascii_string_unchecked(char const * s);
 LEAN_EXPORT lean_obj_res lean_mk_string(char const * s);
 static inline char const * lean_string_cstr(b_lean_obj_arg o) {
     assert(lean_is_string(o));

src/lake/Lake/Build/Common.lean

@@ -5,7 +5,6 @@ Authors: Mac Malone
 -/
 import Lake.Config.Monad
 import Lake.Build.Actions
-import Lake.Util.JsonObject
 
 /-! # Common Build Tools
 This file defines general utilities that abstract common
@@ -32,29 +31,15 @@ which stores information about a (successful) build.
 structure BuildMetadata where
   depHash : Hash
   log : Log
-  deriving ToJson
-
-def BuildMetadata.ofHash (h : Hash) : BuildMetadata :=
-  {depHash := h, log := {}}
-
-def BuildMetadata.fromJson? (json : Json) : Except String BuildMetadata := do
-  let obj ← JsonObject.fromJson? json
-  let depHash ← obj.get "depHash"
-  let log ← obj.getD "log" {}
-  return {depHash, log}
-
-instance : FromJson BuildMetadata := ⟨BuildMetadata.fromJson?⟩
+  deriving ToJson, FromJson
 
 /-- Read persistent trace data from a file. -/
 def readTraceFile? (path : FilePath) : LogIO (Option BuildMetadata) := OptionT.run do
   match (← IO.FS.readFile path |>.toBaseIO) with
   | .ok contents =>
-    if let some hash := Hash.ofString? contents.trim then
-      return .ofHash hash
-    else
-      match Json.parse contents >>= fromJson? with
-      | .ok contents => return contents
-      | .error e => logVerbose s!"{path}: invalid trace file: {e}"; failure
+    match Json.parse contents >>= fromJson? with
+    | .ok contents => return contents
+    | .error e => logVerbose s!"{path}: invalid trace file: {e}"; failure
   | .error (.noFileOrDirectory ..) => failure
   | .error e => logWarning s!"{path}: read failed: {e}"; failure
 
@@ -101,34 +86,25 @@ then `depTrace` / `oldTrace`. No log will be replayed.
   (depTrace : BuildTrace) (traceFile : FilePath) (build : JobM PUnit)
   (action : JobAction := .build) (oldTrace := depTrace.mtime)
 : JobM Bool := do
-  if (← traceFile.pathExists) then
-    if let some data ← readTraceFile? traceFile then
-      if (← checkHashUpToDate info depTrace data.depHash oldTrace) then
-        updateAction .replay
-        data.log.replay
-        return true
-      else
-        go
-    else if (← getIsOldMode) && (← oldTrace.checkUpToDate info) then
+  if let some data ← readTraceFile? traceFile then
+    if (← checkHashUpToDate info depTrace data.depHash oldTrace) then
+      updateAction .replay
+      data.log.replay
       return true
-    else
-      go
+  else if (← getIsOldMode) then
+    if (← oldTrace.checkUpToDate info) then
+      return true
+  else if (← depTrace.checkAgainstTime info) then
+    return true
+  if (← getNoBuild) then
+    IO.Process.exit noBuildCode.toUInt8
   else
-    if (← depTrace.checkAgainstTime info) then
-      return true
-    else
-      go
-where
-  go := do
-    if (← getNoBuild) then
-      IO.Process.exit noBuildCode.toUInt8
-    else
-      updateAction action
-      let iniPos ← getLogPos
-      build -- fatal errors will not produce a trace (or cache their log)
-      let log := (← getLog).takeFrom iniPos
-      writeTraceFile traceFile depTrace log
-      return false
+    updateAction action
+    let iniPos ← getLogPos
+    build -- fatal errors will not produce a trace (or cache their log)
+    let log := (← getLog).takeFrom iniPos
+    writeTraceFile traceFile depTrace log
+    return false
 
 /--
 Checks whether `info` is up-to-date, and runs `build` to recreate it if not.