chore: reordering in Array.Basic

doc/dev/release_checklist.md

@@ -71,12 +71,6 @@ We'll use `v4.6.0` as the intended release version as a running example.
       - Toolchain bump PR including updated Lake manifest
       - Create and push the tag
       - There is no `stable` branch; skip this step
-    - [Verso](https://github.com/leanprover/verso)
-      - Dependencies: exist, but they're not part of the release workflow
-      - The `SubVerso` dependency should be compatible with _every_ Lean release simultaneously, rather than following this workflow
-      - Toolchain bump PR including updated Lake manifest
-      - Create and push the tag
-      - There is no `stable` branch; skip this step
     - [import-graph](https://github.com/leanprover-community/import-graph)
       - Toolchain bump PR including updated Lake manifest
       - Create and push the tag

script/count_versions.sh

@@ -1,21 +0,0 @@
-#!/bin/bash
-# Must be run in a copy of the `lean4` repository, and you'll need to login with `gh auth` first.
-for v in $(gh release list | cut -f1) nightly stable
-do
-  sleep 15 # Don't exceed API rate limits!
-  echo -n $v" "
-  count=$(gh search code --filename lean-toolchain -L 1000 "leanprover/lean4:$v" | wc -l)
-  
-  # Check if version number begins with a 'v'
-  if [[ $v == v* ]]; then
-    sleep 5 # Don't exceed API rate limits!
-    # Remove the leading 'v'
-    v_no_v=${v:1}
-    count_no_v=$(gh search code --filename lean-toolchain -L 1000 "leanprover/lean4:$v_no_v" | wc -l)
-    # Sum the two counts
-    total_count=$(($count + $count_no_v))
-    echo $total_count
-  else
-    echo $count
-  fi
-done | awk '{ printf "%-12s %s\n", $1, $2 }'

script/plot_count_versions.py

@@ -1,50 +0,0 @@
-import matplotlib.pyplot as plt
-import pandas as pd
-import numpy as np
-import sys
-from io import StringIO
-
-# Reading data from stdin
-input_data = sys.stdin.read()
-
-# Using StringIO to simulate a file-like object for pandas
-data_io = StringIO(input_data)
-
-# Reading data into DataFrame
-df = pd.read_csv(data_io, sep="\s+", names=['Version', 'Count'])
-
-# Splitting versions into prefix and suffix
-df['Prefix'] = df['Version'].apply(lambda x: x.split('-')[0])
-df['Suffix'] = df['Version'].apply(lambda x: '-'.join(x.split('-')[1:]) if '-' in x else '')
-
-# Grouping and summing by prefix
-grouped = df.groupby('Prefix').sum().reset_index()
-
-# Setting the color map
-color_map = {'': 'blue'}  # Default color for versions without suffix
-suffixes = df['Suffix'].unique()
-greens = plt.cm.Greens(np.linspace(0.3, 0.9, len(suffixes)))
-
-for i, suffix in enumerate(suffixes):
-    if suffix:  # Assign green shades to versions with suffixes
-        color_map[suffix] = greens[i]
-
-# Plotting the bar chart with new color scheme
-plt.figure(figsize=(10, 6))
-for prefix in grouped['Prefix']:
-    subset = df[df['Prefix'] == prefix]
-    bottom = 0
-    for _, row in subset.iterrows():
-        color = color_map[row['Suffix']]
-        plt.bar(prefix, row['Count'], bottom=bottom, label=row['Version'], color=color)
-        bottom += row['Count']
-
-plt.title('Version Contributions with Distinctive Colors')
-plt.xlabel('Version Prefix')
-plt.ylabel('Count')
-plt.xticks(rotation=45)
-plt.legend(title='Version', bbox_to_anchor=(1.05, 1), loc='upper left')
-
-# Save to a file
-output_file_path = 'version_contribution_chart_colored.png'
-plt.savefig(output_file_path)

src/Init/Data/BitVec/Lemmas.lean

@@ -710,26 +710,6 @@ theorem or_comm (x y : BitVec w) :
   simp [Bool.or_comm]
 instance : Std.Commutative (fun (x y : BitVec w) => x ||| y) := ⟨BitVec.or_comm⟩
 
-@[simp] theorem or_self {x : BitVec w} : x ||| x = x := by
-  ext i
-  simp
-
-@[simp] theorem or_zero {x : BitVec w} : x ||| 0#w = x := by
-  ext i
-  simp
-
-@[simp] theorem zero_or {x : BitVec w} : 0#w ||| x = x := by
-  ext i
-  simp
-
-@[simp] theorem or_allOnes {x : BitVec w} : x ||| allOnes w = allOnes w := by
-  ext i
-  simp
-
-@[simp] theorem allOnes_or {x : BitVec w} : allOnes w ||| x = allOnes w := by
-  ext i
-  simp
-
 /-! ### and -/
 
 @[simp] theorem toNat_and (x y : BitVec v) :
@@ -771,26 +751,6 @@ theorem and_comm (x y : BitVec w) :
   simp [Bool.and_comm]
 instance : Std.Commutative (fun (x y : BitVec w) => x &&& y) := ⟨BitVec.and_comm⟩
 
-@[simp] theorem and_self {x : BitVec w} : x &&& x = x := by
-  ext i
-  simp
-
-@[simp] theorem and_zero {x : BitVec w} : x &&& 0#w = 0#w := by
-  ext i
-  simp
-
-@[simp] theorem zero_and {x : BitVec w} : 0#w &&& x = 0#w := by
-  ext i
-  simp
-
-@[simp] theorem and_allOnes {x : BitVec w} : x &&& allOnes w = x := by
-  ext i
-  simp
-
-@[simp] theorem allOnes_and {x : BitVec w} : allOnes w &&& x = x := by
-  ext i
-  simp
-
 /-! ### xor -/
 
 @[simp] theorem toNat_xor (x y : BitVec v) :
@@ -835,18 +795,6 @@ theorem xor_comm (x y : BitVec w) :
   simp [Bool.xor_comm]
 instance : Std.Commutative (fun (x y : BitVec w) => x ^^^ y) := ⟨BitVec.xor_comm⟩
 
-@[simp] theorem xor_self {x : BitVec w} : x ^^^ x = 0#w := by
-  ext i
-  simp
-
-@[simp] theorem xor_zero {x : BitVec w} : x ^^^ 0#w = x := by
-  ext i
-  simp
-
-@[simp] theorem zero_xor {x : BitVec w} : 0#w ^^^ x = x := by
-  ext i
-  simp
-
 /-! ### not -/
 
 theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
@@ -895,14 +843,6 @@ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
   ext
   simp
 
-@[simp] theorem xor_allOnes {x : BitVec w} : x ^^^ allOnes w = ~~~ x := by
-  ext i
-  simp
-
-@[simp] theorem allOnes_xor {x : BitVec w} : allOnes w ^^^ x = ~~~ x := by
-  ext i
-  simp
-
 /-! ### cast -/
 
 @[simp] theorem not_cast {x : BitVec w} (h : w = w') : ~~~(cast h x) = cast h (~~~x) := by

src/Init/Data/List/Lemmas.lean

@@ -938,38 +938,6 @@ def foldrRecOn {motive : β → Sort _} : ∀ (l : List α) (op : α → β →
         x (mem_cons_self x l) :=
   rfl
 
-/--
-We can prove that two folds over the same list are related (by some arbitrary relation)
-if we know that the initial elements are related and the folding function, for each element of the list,
-preserves the relation.
--/
-theorem foldl_rel {l : List α} {f g : β → α → β} {a b : β} (r : β → β → Prop)
-    (h : r a b) (h' : ∀ (a : α), a ∈ l → ∀ (c c' : β), r c c' → r (f c a) (g c' a)) :
-    r (l.foldl (fun acc a => f acc a) a) (l.foldl (fun acc a => g acc a) b) := by
-  induction l generalizing a b with
-  | nil => simp_all
-  | cons a l ih =>
-    simp only [foldl_cons]
-    apply ih
-    · simp_all
-    · exact fun a m c c' h => h' _ (by simp_all) _ _ h
-
-/--
-We can prove that two folds over the same list are related (by some arbitrary relation)
-if we know that the initial elements are related and the folding function, for each element of the list,
-preserves the relation.
--/
-theorem foldr_rel {l : List α} {f g : α → β → β} {a b : β} (r : β → β → Prop)
-    (h : r a b) (h' : ∀ (a : α), a ∈ l → ∀ (c c' : β), r c c' → r (f a c) (g a c')) :
-    r (l.foldr (fun a acc => f a acc) a) (l.foldr (fun a acc => g a acc) b) := by
-  induction l generalizing a b with
-  | nil => simp_all
-  | cons a l ih =>
-    simp only [foldr_cons]
-    apply h'
-    · simp
-    · exact ih h fun a m c c' h => h' _ (by simp_all) _ _ h
-
 /-! ### getLast -/
 
 theorem getLast_eq_getElem : ∀ (l : List α) (h : l ≠ []),

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean

@@ -35,7 +35,7 @@ Reconstruct bit by bit which value expression must have had which `BitVec` value
 expression - pair values.
 -/
 def reconstructCounterExample (var2Cnf : Std.HashMap BVBit Nat) (assignment : Array (Bool × Nat))
-    (aigSize : Nat) (atomsAssignment : Std.HashMap Nat (Nat × Expr)) :
+    (aigSize : Nat) (atomsAssignment : Std.HashMap Nat Expr) :
     Array (Expr × BVExpr.PackedBitVec) := Id.run do
   let mut sparseMap : Std.HashMap Nat (RBMap Nat Bool Ord.compare) := {}
   for (bitVar, cnfVar) in var2Cnf.toArray do
@@ -70,7 +70,7 @@ def reconstructCounterExample (var2Cnf : Std.HashMap BVBit Nat) (assignment : Ar
       if bitValue then
         value := value ||| (1 <<< currentBit)
       currentBit := currentBit + 1
-    let atomExpr := atomsAssignment.get! bitVecVar |>.snd
+    let atomExpr := atomsAssignment.get! bitVecVar
     finalMap := finalMap.push (atomExpr, ⟨BitVec.ofNat currentBit value⟩)
   return finalMap
 
@@ -83,14 +83,14 @@ structure UnsatProver.Result where
   proof : Expr
   lratCert : LratCert
 
-abbrev UnsatProver := ReflectionResult → Std.HashMap Nat (Nat × Expr) → MetaM UnsatProver.Result
+abbrev UnsatProver := ReflectionResult → Std.HashMap Nat Expr → MetaM UnsatProver.Result
 
 /--
 Contains values that will be used to diagnose spurious counter examples.
 -/
 structure DiagnosisInput where
   unusedHypotheses : Std.HashSet FVarId
-  atomsAssignment : Std.HashMap Nat (Nat × Expr)
+  atomsAssignment : Std.HashMap Nat Expr
 
 /--
 The result of a spurious counter example diagnosis.
@@ -104,14 +104,14 @@ abbrev DiagnosisM : Type → Type := ReaderT DiagnosisInput <| StateRefT Diagnos
 namespace DiagnosisM
 
 def run (x : DiagnosisM Unit) (unusedHypotheses : Std.HashSet FVarId)
-    (atomsAssignment : Std.HashMap Nat (Nat × Expr)) : MetaM Diagnosis := do
+    (atomsAssignment : Std.HashMap Nat Expr) : MetaM Diagnosis := do
   let (_, issues) ← ReaderT.run x { unusedHypotheses, atomsAssignment } |>.run {}
   return issues
 
 def unusedHyps : DiagnosisM (Std.HashSet FVarId) := do
   return (← read).unusedHypotheses
 
-def atomsAssignment : DiagnosisM (Std.HashMap Nat (Nat × Expr)) := do
+def atomsAssignment : DiagnosisM (Std.HashMap Nat Expr) := do
   return (← read).atomsAssignment
 
 def addUninterpretedSymbol (e : Expr) : DiagnosisM Unit :=
@@ -131,7 +131,7 @@ Diagnose spurious counter examples, currently this checks:
 - Whether all hypotheses which contain any variable that was bitblasted were included
 -/
 def diagnose : DiagnosisM Unit := do
-  for (_, (_, expr)) in ← atomsAssignment do
+  for (_, expr) in ← atomsAssignment do
     match_expr expr with
     | BitVec.ofBool x =>
       match x with
@@ -158,7 +158,7 @@ def explainers : List (Diagnosis → Option MessageData) :=
   [uninterpretedExplainer, unusedRelevantHypothesesExplainer]
 
 def explainCounterExampleQuality (unusedHypotheses : Std.HashSet FVarId)
-    (atomsAssignment : Std.HashMap Nat (Nat × Expr)) : MetaM MessageData := do
+    (atomsAssignment : Std.HashMap Nat Expr) : MetaM MessageData := do
   let diagnosis ← DiagnosisM.run DiagnosisM.diagnose unusedHypotheses atomsAssignment
   let folder acc explainer := if let some m := explainer diagnosis then acc.push m else acc
   let explanations := explainers.foldl (init := #[]) folder
@@ -172,7 +172,7 @@ def explainCounterExampleQuality (unusedHypotheses : Std.HashSet FVarId)
     return err
 
 def lratBitblaster (cfg : TacticContext) (reflectionResult : ReflectionResult)
-    (atomsAssignment : Std.HashMap Nat (Nat × Expr)) :
+    (atomsAssignment : Std.HashMap Nat Expr) :
     MetaM UnsatProver.Result := do
   let bvExpr := reflectionResult.bvExpr
   let entry ←
@@ -242,7 +242,7 @@ def closeWithBVReflection (g : MVarId) (unsatProver : UnsatProver) :
         reflectBV g
     trace[Meta.Tactic.bv] "Reflected bv logical expression: {reflectionResult.bvExpr}"
 
-    let atomsPairs := (← getThe State).atoms.toList.map (fun (expr, ⟨width, ident⟩) => (ident, (width, expr)))
+    let atomsPairs := (← getThe State).atoms.toList.map (fun (expr, _, ident) => (ident, expr))
     let atomsAssignment := Std.HashMap.ofList atomsPairs
     let ⟨bvExprUnsat, cert⟩ ← unsatProver reflectionResult atomsAssignment
     let proveFalse ← reflectionResult.proveFalse bvExprUnsat

src/Lean/Elab/Tactic/BVDecide/Frontend/LRAT.lean

@@ -141,11 +141,10 @@ This will obtain an `LratCert` if the formula is UNSAT and throw errors otherwis
 def runExternal (cnf : CNF Nat) (solver : System.FilePath) (lratPath : System.FilePath)
     (trimProofs : Bool) (timeout : Nat) (binaryProofs : Bool)
     : MetaM (Except (Array (Bool × Nat)) LratCert) := do
-  IO.FS.withTempFile fun cnfHandle cnfPath => do
+  IO.FS.withTempFile fun _ cnfPath => do
     withTraceNode `sat (fun _ => return "Serializing SAT problem to DIMACS file") do
       -- lazyPure to prevent compiler lifting
-      cnfHandle.putStr  (← IO.lazyPure (fun _ => cnf.dimacs))
-      cnfHandle.flush
+      IO.FS.writeFile cnfPath (← IO.lazyPure (fun _ => cnf.dimacs))
 
     let res ←
       withTraceNode `sat (fun _ => return "Running SAT solver") do

src/Lean/Elab/Tactic/Basic.lean

@@ -49,9 +49,6 @@ instance : Monad TacticM :=
   let i := inferInstanceAs (Monad TacticM);
   { pure := i.pure, bind := i.bind }
 
-instance : Inhabited (TacticM α) where
-  default := fun _ _ => default
-
 def getGoals : TacticM (List MVarId) :=
   return (← get).goals
 

src/Lean/Meta/Instances.lean

@@ -113,34 +113,8 @@ For example:
     (because A B are out-params and are only filled in once we synthesize 2)
 
 (The type of `inst` must not contain mvars.)
-
-Remark: `projInfo?` is `some` if the instance is a projection.
-We need this information because of the heuristic we use to annotate binder
-information in projections. See PR #5376 and issue #5333. Before PR
-#5376, given a class `C` at
-```
-class A (n : Nat) where
-
-instance [A n] : A n.succ where
-
-class B [A 20050] where
-
-class C [A 20000] extends B where
-```
-we would get the following instance
-```
-C.toB [inst : A 20000] [self : @C inst] : @B ...
-```
-After the PR, we have
-```
-C.toB {inst : A 20000} [self : @C inst] : @B ...
-```
-Note the attribute `inst` is now just a regular implicit argument.
-To ensure `computeSynthOrder` works as expected, we should take
-this change into account while processing field `self`.
-This field is the one at position `projInfo?.numParams`.
 -/
-private partial def computeSynthOrder (inst : Expr) (projInfo? : Option ProjectionFunctionInfo) : MetaM (Array Nat) :=
+private partial def computeSynthOrder (inst : Expr) : MetaM (Array Nat) :=
   withReducible do
   let instTy ← inferType inst
 
@@ -177,8 +151,7 @@ private partial def computeSynthOrder (inst : Expr) (projInfo? : Option Projecti
   let tyOutParams ← getSemiOutParamPositionsOf ty
   let tyArgs := ty.getAppArgs
   for tyArg in tyArgs, i in [:tyArgs.size] do
-    unless tyOutParams.contains i do
-      assignMVarsIn tyArg
+    unless tyOutParams.contains i do assignMVarsIn tyArg
 
   -- Now we successively try to find the next ready subgoal, where all
   -- non-out-params are mvar-free.
@@ -186,13 +159,7 @@ private partial def computeSynthOrder (inst : Expr) (projInfo? : Option Projecti
   let mut toSynth := List.range argMVars.size |>.filter (argBIs[·]! == .instImplicit) |>.toArray
   while !toSynth.isEmpty do
     let next? ← toSynth.findM? fun i => do
-      let argTy ← instantiateMVars (← inferType argMVars[i]!)
-      if let some projInfo := projInfo? then
-        if projInfo.numParams == i then
-          -- See comment regarding `projInfo?` at the beginning of this function
-          assignMVarsIn argTy
-          return true
-      forallTelescopeReducing argTy fun _ argTy => do
+      forallTelescopeReducing (← instantiateMVars (← inferType argMVars[i]!)) fun _ argTy => do
       let argTy ← whnf argTy
       let argOutParams ← getSemiOutParamPositionsOf argTy
       let argTyArgs := argTy.getAppArgs
@@ -228,8 +195,7 @@ def addInstance (declName : Name) (attrKind : AttributeKind) (prio : Nat) : Meta
   let c ← mkConstWithLevelParams declName
   let keys ← mkInstanceKey c
   addGlobalInstance declName attrKind
-  let projInfo? ← getProjectionFnInfo? declName
-  let synthOrder ← computeSynthOrder c projInfo?
+  let synthOrder ← computeSynthOrder c
   instanceExtension.add { keys, val := c, priority := prio, globalName? := declName, attrKind, synthOrder } attrKind
 
 builtin_initialize

src/Lean/Meta/Tactic/Refl.lean

@@ -12,9 +12,6 @@ namespace Lean.Meta
 
 /--
 Close given goal using `Eq.refl`.
-
-See `Lean.MVarId.applyRfl` for the variant that also consults `@[refl]` lemmas, and which
-backs the `rfl` tactic.
 -/
 def _root_.Lean.MVarId.refl (mvarId : MVarId) : MetaM Unit := do
   mvarId.withContext do

src/Lean/Meta/Tactic/Rfl.lean

@@ -50,59 +50,33 @@ open Elab Tactic
 
 /-- `MetaM` version of the `rfl` tactic.
 
-This tactic applies to a goal whose target has the form `x ~ x`, where `~` is a reflexive
-relation, that is, equality or another relation which has a reflexive lemma tagged with the
-attribute [refl].
+This tactic applies to a goal whose target has the form `x ~ x`,
+where `~` is a reflexive relation other than `=`,
+that is, a relation which has a reflexive lemma tagged with the attribute @[refl].
 -/
-def _root_.Lean.MVarId.applyRfl (goal : MVarId) : MetaM Unit := goal.withContext do
-  -- NB: uses whnfR, we do not want to unfold the relation itself
-  let t ← whnfR <|← instantiateMVars <|← goal.getType
-  if t.getAppNumArgs < 2 then
-    throwError "rfl can only be used on binary relations, not{indentExpr (← goal.getType)}"
-
-  -- Special case HEq here as it has a different argument order.
-  if t.isAppOfArity ``HEq 4 then
-    let gs ← goal.applyConst ``HEq.refl
-    unless gs.isEmpty do
-      throwError MessageData.tagged `Tactic.unsolvedGoals <| m!"unsolved goals\n{
-        goalsToMessageData gs}"
-    return
-
-  let rel := t.appFn!.appFn!
-  let lhs := t.appFn!.appArg!
-  let rhs := t.appArg!
-
-  let success ← approxDefEq <| isDefEqGuarded lhs rhs
-  unless success do
-    let explanation := MessageData.ofLazyM (es := #[lhs, rhs]) do
-      let (lhs, rhs) ← addPPExplicitToExposeDiff lhs rhs
-      return m!"The lhs{indentExpr lhs}\nis not definitionally equal to rhs{indentExpr rhs}"
-    throwTacticEx `apply_rfl goal explanation
-
-  if rel.isAppOfArity `Eq 1 then
-    -- The common case is equality: just use `Eq.refl`
-    let us := rel.appFn!.constLevels!
-    let α :=  rel.appArg!
-    goal.assign (mkApp2 (mkConst ``Eq.refl us) α lhs)
+def _root_.Lean.MVarId.applyRfl (goal : MVarId) : MetaM Unit := do
+  let .app (.app rel _) _ ← whnfR <|← instantiateMVars <|← goal.getType
+    | throwError "reflexivity lemmas only apply to binary relations, not{
+        indentExpr (← goal.getType)}"
+  if let .app (.const ``Eq [_]) _ := rel then
+    throwError "MVarId.applyRfl does not solve `=` goals. Use `MVarId.refl` instead."
   else
-    -- Else search through `@refl` keyed by the relation
     let s ← saveState
     let mut ex? := none
     for lem in ← (reflExt.getState (← getEnv)).getMatch rel reflExt.config do
       try
         let gs ← goal.apply (← mkConstWithFreshMVarLevels lem)
         if gs.isEmpty then return () else
-          throwError MessageData.tagged `Tactic.unsolvedGoals <| m!"unsolved goals\n{
+          logError <| MessageData.tagged `Tactic.unsolvedGoals <| m!"unsolved goals\n{
             goalsToMessageData gs}"
       catch e =>
-        unless ex?.isSome do
-          ex? := some (← saveState, e) -- stash the first failure of `apply`
+        ex? := ex? <|> (some (← saveState, e)) -- stash the first failure of `apply`
       s.restore
     if let some (sErr, e) := ex? then
       sErr.restore
       throw e
     else
-      throwError "rfl failed, no @[refl] lemma registered for relation{indentExpr rel}"
+      throwError "rfl failed, no lemma with @[refl] applies"
 
 /-- Helper theorem for `Lean.MVarId.liftReflToEq`. -/
 private theorem rel_of_eq_and_refl {α : Sort _} {R : α → α → Prop}

src/Lean/ProjFns.lean

@@ -21,7 +21,7 @@ structure ProjectionFunctionInfo where
   i : Nat
   /-- `true` if the structure is a class. -/
   fromClass : Bool
-  deriving Inhabited, Repr
+  deriving Inhabited
 
 @[export lean_mk_projection_info]
 def mkProjectionInfoEx (ctorName : Name) (numParams : Nat) (i : Nat) (fromClass : Bool) : ProjectionFunctionInfo :=

src/Std/Data/DHashMap/Basic.lean

@@ -186,15 +186,6 @@ section Unverified
     (init : δ) (b : DHashMap α β) : δ :=
   b.1.fold f init
 
-/-- Partition a hashset into two hashsets based on a predicate. -/
-@[inline] def partition (f : (a : α) → β a → Bool)
-    (m : DHashMap α β) : DHashMap α β × DHashMap α β :=
-  m.fold (init := (∅, ∅)) fun ⟨l, r⟩  a b =>
-    if f a b then
-      (l.insert a b, r)
-    else
-      (l, r.insert a b)
-
 @[inline, inherit_doc Raw.forM] def forM (f : (a : α) → β a → m PUnit)
     (b : DHashMap α β) : m PUnit :=
   b.1.forM f
@@ -269,10 +260,6 @@ instance [BEq α] [Hashable α] : ForIn m (DHashMap α β) ((a : α) × β a) wh
     DHashMap α (fun _ => Unit) :=
   Const.insertManyUnit ∅ l
 
-@[inline, inherit_doc Raw.Const.unitOfArray] def Const.unitOfArray [BEq α] [Hashable α] (l : Array α) :
-    DHashMap α (fun _ => Unit) :=
-  Const.insertManyUnit ∅ l
-
 @[inherit_doc Raw.Internal.numBuckets] def Internal.numBuckets
     (m : DHashMap α β) : Nat :=
   Raw.Internal.numBuckets m.1

src/Std/Data/DHashMap/Raw.lean

@@ -411,14 +411,6 @@ This is mainly useful to implement `HashSet.ofList`, so if you are considering u
     Raw α (fun _ => Unit) :=
   Const.insertManyUnit ∅ l
 
-/-- Creates a hash map from an array of keys, associating the value `()` with each key.
-
-This is mainly useful to implement `HashSet.ofArray`, so if you are considering using this,
-`HashSet` or `HashSet.Raw` might be a better fit for you. -/
-@[inline] def Const.unitOfArray [BEq α] [Hashable α] (l : Array α) :
-    Raw α (fun _ => Unit) :=
-  Const.insertManyUnit ∅ l
-
 /--
 Returns the number of buckets in the internal representation of the hash map. This function may be
 useful for things like monitoring system health, but it should be considered an internal

src/Std/Data/HashMap/Basic.lean

@@ -190,11 +190,6 @@ section Unverified
     (m : HashMap α β) : HashMap α β :=
   ⟨m.inner.filter f⟩
 
-@[inline, inherit_doc DHashMap.partition] def partition (f : α → β → Bool)
-    (m : HashMap α β) : HashMap α β × HashMap α β :=
-  let ⟨l, r⟩ := m.inner.partition f
-  ⟨⟨l⟩, ⟨r⟩⟩
-
 @[inline, inherit_doc DHashMap.foldM] def foldM {m : Type w → Type w}
     [Monad m] {γ : Type w} (f : γ → α → β → m γ) (init : γ) (b : HashMap α β) : m γ :=
   b.inner.foldM f init
@@ -255,10 +250,6 @@ instance [BEq α] [Hashable α] {m : Type w → Type w} : ForIn m (HashMap α β
     HashMap α Unit :=
   ⟨DHashMap.Const.unitOfList l⟩
 
-@[inline, inherit_doc DHashMap.Const.unitOfArray] def unitOfArray [BEq α] [Hashable α] (l : Array α) :
-    HashMap α Unit :=
-  ⟨DHashMap.Const.unitOfArray l⟩
-
 @[inline, inherit_doc DHashMap.Internal.numBuckets] def Internal.numBuckets
     (m : HashMap α β) : Nat :=
   DHashMap.Internal.numBuckets m.inner

src/Std/Data/HashSet/Basic.lean

@@ -158,11 +158,6 @@ section Unverified
 @[inline] def filter (f : α → Bool) (m : HashSet α) : HashSet α :=
   ⟨m.inner.filter fun a _ => f a⟩
 
-/-- Partition a hashset into two hashsets based on a predicate. -/
-@[inline] def partition (f : α → Bool) (m : HashSet α) : HashSet α × HashSet α :=
-  let ⟨l, r⟩ := m.inner.partition fun a _ => f a
-  ⟨⟨l⟩, ⟨r⟩⟩
-
 /--
 Monadically computes a value by folding the given function over the elements in the hash set in some
 order.
@@ -217,14 +212,6 @@ in the collection will be present in the returned hash set.
 @[inline] def ofList [BEq α] [Hashable α] (l : List α) : HashSet α :=
   ⟨HashMap.unitOfList l⟩
 
-/--
-Creates a hash set from an array of elements. Note that unlike repeatedly calling `insert`, if the
-collection contains multiple elements that are equal (with regard to `==`), then the last element
-in the collection will be present in the returned hash set.
--/
-@[inline] def ofArray [BEq α] [Hashable α] (l : Array α) : HashSet α :=
-  ⟨HashMap.unitOfArray l⟩
-
 /-- Computes the union of the given hash sets. -/
 @[inline] def union [BEq α] [Hashable α] (m₁ m₂ : HashSet α) : HashSet α :=
   m₂.fold (init := m₁) fun acc x => acc.insert x

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean

@@ -142,8 +142,8 @@ def toString : BVUnOp → String
   | not => "~"
   | shiftLeftConst n => s!"<< {n}"
   | shiftRightConst n => s!">> {n}"
-  | rotateLeft n => s!"rotL {n}"
-  | rotateRight n => s!"rotR {n}"
+  | rotateLeft n => s! "rotL {n}"
+  | rotateRight n => s! "rotR {n}"
   | arithShiftRightConst n => s!">>a {n}"
 
 instance : ToString BVUnOp := ⟨toString⟩
@@ -238,7 +238,7 @@ def toString : BVExpr w → String
   | .var idx => s!"var{idx}"
   | .const val => ToString.toString val
   | .zeroExtend v expr => s!"(zext {v} {expr.toString})"
-  | .extract start len expr => s!"{expr.toString}[{start}, {len}]"
+  | .extract hi lo expr => s!"{expr.toString}[{hi}:{lo}]"
   | .bin lhs op rhs => s!"({lhs.toString} {op.toString} {rhs.toString})"
   | .un op operand => s!"({op.toString} {toString operand})"
   | .append lhs rhs => s!"({toString lhs} ++ {toString rhs})"

src/library/constructions/projection.cpp

@@ -63,8 +63,6 @@ environment mk_projections(environment const & env, name const & n, buffer<name>
             // 1. The original binder before `mk_outparam_args_implicit` is not an instance implicit.
             // 2. It is not originally an outparam. Outparams must be implicit.
             bi = mk_binder_info();
-        } else if (is_inst_implicit(bi_orig) && inst_implicit) {
-            bi = mk_implicit_binder_info();
         }
         expr param = lctx.mk_local_decl(ngen, binding_name(cnstr_type), type, bi);
         cnstr_type = instantiate(binding_body(cnstr_type), param);

tests/lean/run/5333.lean

@@ -1,20 +0,0 @@
-class A (n : Nat) where
-
-instance [A n] : A n.succ where
-
-class B [A 20050] where
-
-set_option trace.Meta.debug true
-
-class C [A 20000] extends B where
-
-#check C.toB
-
-instance : A 20050 where
-
-class D where
-
-instance inst1 : D where
-instance inst2 [B] : D where
-
-#synth D

tests/lean/run/rflApplyFoApprox.lean

@@ -1,15 +0,0 @@
-
-opaque f : Nat → Nat
--- A rewrite with a free variable on the RHS
-
-opaque P : Nat → (Nat → Nat) → Prop
-opaque Q : Nat → Prop
-opaque foo (g : Nat → Nat) (x : Nat) : P x f ↔ Q (g x) := sorry
-
-example : P x f ↔ Q (x + 10) := by
-  rewrite [foo]
-  -- we have an mvar now
-  with_reducible rfl -- should should instantiate it with the lambda on the RHS and close the goal
-  -- same as
-  -- with_reducible (apply (Iff.refl _))
-  -- NB: apply, not exact! Different defEq flags.

tests/lean/run/rflTacticErrors.lean

@@ -1,445 +0,0 @@
-
-/-!
-This file tests the `rfl` tactic:
- * Extensibility
- * Error messages
- * Effect of `with_reducible`
--/
-
--- First, let's see what `rfl` does:
-
-/--
-error: 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.
-⊢ false = true
--/
-#guard_msgs in
-example : false = true := by rfl
-
--- Now to `apply_rfl`.
-
--- A plain reflexive predicate
-inductive P : α → α → Prop where | refl : P a a
-attribute [refl] P.refl
-
--- Plain error
-
-/--
-error: tactic 'apply_rfl' failed, The lhs
-  42
-is not definitionally equal to rhs
-  23
-⊢ P 42 23
--/
-#guard_msgs in
-example : P 42 23 := by apply_rfl
-
--- Revealing implicit arguments
-
-opaque withImplicitNat {n : Nat} : Nat
-
-/--
-error: tactic 'apply_rfl' failed, The lhs
-  @withImplicitNat 42
-is not definitionally equal to rhs
-  @withImplicitNat 23
-⊢ P withImplicitNat withImplicitNat
--/
-#guard_msgs in
-example : P (@withImplicitNat 42) (@withImplicitNat 23) := by apply_rfl
-
-
--- Exhaustive testing of various combinations:
-
--- In addition to Eq, HEq and Iff  we test four relations:
-
-
--- Defeq to relation `P` at reducible transparency
-abbrev Q : α → α → Prop := P
-
--- Defeq to relation `P` at default transparency
-def Q' : α → α → Prop := P
-
--- No refl attribute
-inductive R : α → α → Prop where | refl : R a a
-
-
-/-
-Now we systematically test all relations with
-* syntactic equal arguments
-* reducibly equal arguments
-* semireducibly equal arguments
-* nonequal arguments
-
-and all using `apply_rfl` and `with_reducible apply_rfl`
--/
-
-
--- Syntactic equal
-
-example : true = true   := by apply_rfl
-example : HEq true true := by apply_rfl
-example : True ↔ True   := by apply_rfl
-example : P true true   := by apply_rfl
-example : Q true true   := by apply_rfl
-/--
-error: rfl failed, no @[refl] lemma registered for relation
-  Q'
--/
-#guard_msgs in example : Q' true true  := by apply_rfl -- Error
-/--
-error: rfl failed, no @[refl] lemma registered for relation
-  R
--/
-#guard_msgs in example : R true true   := by apply_rfl -- Error
-
-example : true = true   := by with_reducible apply_rfl
-example : HEq true true := by with_reducible apply_rfl
-example : True ↔ True   := by with_reducible apply_rfl
-example : P true true   := by with_reducible apply_rfl
-example : Q true true   := by with_reducible apply_rfl
-/--
-error: rfl failed, no @[refl] lemma registered for relation
-  Q'
--/
-#guard_msgs in
-example : Q' true true  := by with_reducible apply_rfl -- Error
-/--
-error: rfl failed, no @[refl] lemma registered for relation
-  R
--/
-#guard_msgs in
-example : R true true   := by with_reducible apply_rfl -- Error
-
--- Reducibly equal
-
-abbrev true' := true
-abbrev True' := True
-
-example : true' = true   := by apply_rfl
-example : HEq true' true := by apply_rfl
-example : True' ↔ True   := by apply_rfl
-example : P true' true   := by apply_rfl
-example : Q true' true   := by apply_rfl
-/--
-error: rfl failed, no @[refl] lemma registered for relation
-  Q'
--/
-#guard_msgs in
-example : Q' true' true  := by apply_rfl -- Error
-/--
-error: rfl failed, no @[refl] lemma registered for relation
-  R
--/
-#guard_msgs in
-example : R true' true   := by apply_rfl -- Error
-
-example : true' = true   := by with_reducible apply_rfl
-example : HEq true' true := by with_reducible apply_rfl
-example : True' ↔ True   := by with_reducible apply_rfl
-example : P true' true   := by with_reducible apply_rfl
-example : Q true' true   := by with_reducible apply_rfl -- NB: No error, Q and true' reducible
-/--
-error: rfl failed, no @[refl] lemma registered for relation
-  Q'
--/
-#guard_msgs in
-example : Q' true' true  := by with_reducible apply_rfl -- Error
-/--
-error: rfl failed, no @[refl] lemma registered for relation
-  R
--/
-#guard_msgs in
-example : R true' true   := by with_reducible apply_rfl -- Error
-
--- Equal at default transparency only
-
-def true'' := true
-def True'' := True
-
-example : true'' = true   := by apply_rfl
-example : HEq true'' true := by apply_rfl
-example : True'' ↔ True   := by apply_rfl
-example : P true'' true   := by apply_rfl
-example : Q true'' true   := by apply_rfl
-/--
-error: rfl failed, no @[refl] lemma registered for relation
-  Q'
--/
-#guard_msgs in
-example : Q' true'' true  := by apply_rfl -- Error
-/--
-error: rfl failed, no @[refl] lemma registered for relation
-  R
--/
-#guard_msgs in
-example : R true'' true   := by apply_rfl -- Error
-
-/--
-error: tactic 'apply_rfl' failed, The lhs
-  true''
-is not definitionally equal to rhs
-  true
-⊢ true'' = true
--/
-#guard_msgs in
-example : true'' = true   := by with_reducible apply_rfl -- Error
-/--
-error: tactic 'apply' failed, failed to unify
-  @HEq ?α ?a ?α ?a
-with
-  @HEq Bool true'' Bool true
-⊢ HEq true'' true
--/
-#guard_msgs in
-example : HEq true'' true := by with_reducible apply_rfl -- Error
-/--
-error: tactic 'apply_rfl' failed, The lhs
-  True''
-is not definitionally equal to rhs
-  True
-⊢ True'' ↔ True
--/
-#guard_msgs in
-example : True'' ↔ True   := by with_reducible apply_rfl -- Error
-/--
-error: tactic 'apply_rfl' failed, The lhs
-  true''
-is not definitionally equal to rhs
-  true
-⊢ P true'' true
--/
-#guard_msgs in
-example : P true'' true   := by with_reducible apply_rfl -- Error
-/--
-error: tactic 'apply_rfl' failed, The lhs
-  true''
-is not definitionally equal to rhs
-  true
-⊢ Q true'' true
--/
-#guard_msgs in
-example : Q true'' true   := by with_reducible apply_rfl -- Error
-/--
-error: tactic 'apply_rfl' failed, The lhs
-  true''
-is not definitionally equal to rhs
-  true
-⊢ Q' true'' true
--/
-#guard_msgs in
-example : Q' true'' true  := by with_reducible apply_rfl -- Error
-/--
-error: tactic 'apply_rfl' failed, The lhs
-  true''
-is not definitionally equal to rhs
-  true
-⊢ R true'' true
--/
-#guard_msgs in
-example : R true'' true   := by with_reducible apply_rfl -- Error
-
--- Unequal
-/--
-error: tactic 'apply_rfl' failed, The lhs
-  false
-is not definitionally equal to rhs
-  true
-⊢ false = true
--/
-#guard_msgs in
-example : false = true   := by apply_rfl -- Error
-/--
-error: tactic 'apply' failed, failed to unify
-  HEq ?a ?a
-with
-  HEq false true
-⊢ HEq false true
--/
-#guard_msgs in
-example : HEq false true := by apply_rfl -- Error
-/--
-error: tactic 'apply_rfl' failed, The lhs
-  False
-is not definitionally equal to rhs
-  True
-⊢ False ↔ True
--/
-#guard_msgs in
-example : False ↔ True   := by apply_rfl -- Error
-/--
-error: tactic 'apply_rfl' failed, The lhs
-  false
-is not definitionally equal to rhs
-  true
-⊢ P false true
--/
-#guard_msgs in
-example : P false true   := by apply_rfl -- Error
-/--
-error: tactic 'apply_rfl' failed, The lhs
-  false
-is not definitionally equal to rhs
-  true
-⊢ Q false true
--/
-#guard_msgs in
-example : Q false true   := by apply_rfl -- Error
-/--
-error: tactic 'apply_rfl' failed, The lhs
-  false
-is not definitionally equal to rhs
-  true
-⊢ Q' false true
--/
-#guard_msgs in
-example : Q' false true  := by apply_rfl -- Error
-/--
-error: tactic 'apply_rfl' failed, The lhs
-  false
-is not definitionally equal to rhs
-  true
-⊢ R false true
--/
-#guard_msgs in
-example : R false true   := by apply_rfl -- Error
-
-/--
-error: tactic 'apply_rfl' failed, The lhs
-  false
-is not definitionally equal to rhs
-  true
-⊢ false = true
--/
-#guard_msgs in
-example : false = true   := by with_reducible apply_rfl -- Error
-/--
-error: tactic 'apply' failed, failed to unify
-  HEq ?a ?a
-with
-  HEq false true
-⊢ HEq false true
--/
-#guard_msgs in
-example : HEq false true := by with_reducible apply_rfl -- Error
-/--
-error: tactic 'apply_rfl' failed, The lhs
-  False
-is not definitionally equal to rhs
-  True
-⊢ False ↔ True
--/
-#guard_msgs in
-example : False ↔ True   := by with_reducible apply_rfl -- Error
-/--
-error: tactic 'apply_rfl' failed, The lhs
-  false
-is not definitionally equal to rhs
-  true
-⊢ P false true
--/
-#guard_msgs in
-example : P false true   := by with_reducible apply_rfl -- Error
-/--
-error: tactic 'apply_rfl' failed, The lhs
-  false
-is not definitionally equal to rhs
-  true
-⊢ Q false true
--/
-#guard_msgs in
-example : Q false true   := by with_reducible apply_rfl -- Error
-/--
-error: tactic 'apply_rfl' failed, The lhs
-  false
-is not definitionally equal to rhs
-  true
-⊢ Q' false true
--/
-#guard_msgs in
-example : Q' false true  := by with_reducible apply_rfl -- Error
-/--
-error: tactic 'apply_rfl' failed, The lhs
-  false
-is not definitionally equal to rhs
-  true
-⊢ R false true
--/
-#guard_msgs in
-example : R false true   := by with_reducible apply_rfl -- Error
-
--- Inheterogeneous unequal
-
-/--
-error: tactic 'apply' failed, failed to unify
-  HEq ?a ?a
-with
-  HEq true 1
-⊢ HEq true 1
--/
-#guard_msgs in
-example : HEq true 1 := by apply_rfl -- Error
-/--
-error: tactic 'apply' failed, failed to unify
-  HEq ?a ?a
-with
-  HEq true 1
-⊢ HEq true 1
--/
-#guard_msgs in
-example : HEq true 1 := by with_reducible apply_rfl -- Error
-
--- Rfl lemma with side condition:
--- Error message should show left-over goal
-
-inductive S : Bool → Bool → Prop where | refl : a = true → S a a
-attribute [refl] S.refl
-/--
-error: tactic 'apply_rfl' failed, The lhs
-  true
-is not definitionally equal to rhs
-  false
-⊢ S true false
--/
-#guard_msgs in
-example : S true false  := by apply_rfl -- Error
-/--
-error: tactic 'apply_rfl' failed, The lhs
-  true
-is not definitionally equal to rhs
-  false
-⊢ S true false
--/
-#guard_msgs in
-example : S true false  := by with_reducible apply_rfl -- Error
-/--
-error: unsolved goals
-case a
-⊢ true = true
--/
-#guard_msgs in
-example : S true true   := by apply_rfl -- Error (left-over goal)
-/--
-error: unsolved goals
-case a
-⊢ true = true
--/
-#guard_msgs in
-example : S true true   := by with_reducible apply_rfl -- Error (left-over goal)
-/--
-error: unsolved goals
-case a
-⊢ false = true
--/
-#guard_msgs in
-example : S false false := by apply_rfl -- Error (left-over goal)
-/--
-error: unsolved goals
-case a
-⊢ false = true
--/
-#guard_msgs in
-example : S false false := by with_reducible apply_rfl -- Error (left-over goal)

tests/lean/run/synthOrderRegression.lean

@@ -1,19 +0,0 @@
--- Artificial example for exposing a regression introduced while working on PR #5376
--- fix: modify projection instance binder info
-
-class Foo (α : Type) [Add α] where
-   bla : [Mul α] → BEq α
-
-attribute [instance] Foo.bla
-
-inductive Boo where
-  | unit
-
-instance : Add Boo where
-  add _ _ := .unit
-
-instance : Mul Boo where
-  mul _ _ := .unit
-
-def f [Foo Boo] (a b : Boo) : Bool :=
-  a == b

tests/lean/synthorder.lean.expected.out

@@ -11,10 +11,13 @@ all remaining arguments have metavariables:
       Foo A B
       Foo B C
 [Meta.synthOrder] synthesizing the arguments of @instFooOption in the order []:
-[Meta.synthOrder] synthesizing the arguments of @TwoHalf.toTwo in the order [2]:
+[Meta.synthOrder] synthesizing the arguments of @TwoHalf.toTwo in the order [1, 2]:
+      One α
       TwoHalf α
-[Meta.synthOrder] synthesizing the arguments of @Four.toThree in the order [4]:
+[Meta.synthOrder] synthesizing the arguments of @Four.toThree in the order [4, 2, 3]:
       Four α β
+      One β
+      TwoHalf β
 [Meta.synthOrder] synthesizing the arguments of @instFourOfThree in the order [4, 2, 3]:
       Three α β
       One β