more

src/Lean/Compiler/LCNF/JoinPoints.lean

@@ -39,12 +39,12 @@ structure FindState where
   /--
   All current join point candidates accessible by their `FVarId`.
   -/
-  candidates : Std.HashMap FVarId CandidateInfo := .empty
+  candidates : Std.HashMap FVarId CandidateInfo := ∅
   /--
   The `FVarId`s of all `fun` declarations that were declared within the
   current `fun`.
   -/
-  scope : Std.HashSet FVarId := .empty
+  scope : Std.HashSet FVarId := ∅
 
 abbrev ReplaceCtx := Std.HashMap FVarId Name
 
@@ -88,7 +88,7 @@ private partial def removeCandidatesInLetValue (e : LetValue) : FindM Unit := do
 Add a new join point candidate to the state.
 -/
 private def addCandidate (fvarId : FVarId) (arity : Nat) : FindM Unit := do
-  let cinfo := { arity, associated := .empty }
+  let cinfo := { arity, associated := ∅ }
   modifyCandidates (fun cs => cs.insert fvarId cinfo )
 
 /--
@@ -177,7 +177,7 @@ and all calls to them with `jmp`s.
 -/
 partial def replace (decl : Decl) (state : FindState) : CompilerM Decl := do
   let mapper := fun acc cname _ => do return acc.insert cname (← mkFreshJpName)
-  let replaceCtx : ReplaceCtx ← state.candidates.foldM (init := .empty) mapper
+  let replaceCtx : ReplaceCtx ← state.candidates.foldM (init := ∅) mapper
   let newValue ← decl.value.mapCodeM go |>.run replaceCtx
   return { decl with value := newValue }
 where

src/Lean/Data/NameMap.lean

@@ -81,7 +81,7 @@ end NameSSet
 def NameHashSet := Std.HashSet Name
 
 namespace NameHashSet
-@[inline] def empty : NameHashSet := Std.HashSet.empty
+@[inline] def empty : NameHashSet := (∅ : Std.HashSet Name)
 instance : EmptyCollection NameHashSet := ⟨empty⟩
 instance : Inhabited NameHashSet := ⟨{}⟩
 def insert (s : NameHashSet) (n : Name) := Std.HashSet.insert s n

src/Lean/Elab/Tactic/Omega/OmegaM.lean

@@ -73,7 +73,7 @@ abbrev OmegaM := StateRefT Cache OmegaM'
 
 /-- Run a computation in the `OmegaM` monad, starting with no recorded atoms. -/
 def OmegaM.run (m : OmegaM α) (cfg : OmegaConfig) : MetaM α :=
-  m.run' Std.HashMap.empty |>.run' {} { cfg } |>.run'
+  m.run' (∅ : Std.HashMap ..) |>.run' {} { cfg } |>.run'
 
 /-- Retrieve the user-specified configuration options. -/
 def cfg : OmegaM OmegaConfig := do pure (← read).cfg
@@ -168,7 +168,7 @@ def analyzeAtom (e : Expr) : OmegaM (Std.HashSet Expr) := do
   match e.getAppFnArgs with
   | (``Nat.cast, #[.const ``Int [], _, e']) =>
     -- Casts of natural numbers are non-negative.
-    let mut r := Std.HashSet.empty.insert (Expr.app (.const ``Int.ofNat_nonneg []) e')
+    let mut r := (∅ : Std.HashSet Expr).insert (Expr.app (.const ``Int.ofNat_nonneg []) e')
     match (← cfg).splitNatSub, e'.getAppFnArgs with
       | true, (``HSub.hSub, #[_, _, _, _, a, b]) =>
         -- `((a - b : Nat) : Int)` gives a dichotomy
@@ -190,7 +190,7 @@ def analyzeAtom (e : Expr) : OmegaM (Std.HashSet Expr) := do
       let ne_zero := mkApp3 (.const ``Ne [1]) (.const ``Int []) k (toExpr (0 : Int))
       let pos := mkApp4 (.const ``LT.lt [0]) (.const ``Int []) (.const ``Int.instLTInt [])
         (toExpr (0 : Int)) k
-      pure <| Std.HashSet.empty.insert
+      pure <| (∅ : Std.HashSet Expr).insert
         (mkApp3 (.const ``Int.mul_ediv_self_le []) x k (← mkDecideProof ne_zero)) |>.insert
           (mkApp3 (.const ``Int.lt_mul_ediv_self_add []) x k (← mkDecideProof pos))
   | (``HMod.hMod, #[_, _, _, _, x, k]) =>
@@ -202,7 +202,7 @@ def analyzeAtom (e : Expr) : OmegaM (Std.HashSet Expr) := do
         let b_pos := mkApp4 (.const ``LT.lt [0]) (.const ``Int []) (.const ``Int.instLTInt [])
           (toExpr (0 : Int)) b
         let pow_pos := mkApp3 (.const ``Lean.Omega.Int.pos_pow_of_pos []) b exp (← mkDecideProof b_pos)
-        pure <| Std.HashSet.empty.insert
+        pure <| (∅ : Std.HashSet Expr).insert
           (mkApp3 (.const ``Int.emod_nonneg []) x k
               (mkApp3 (.const ``Int.ne_of_gt []) k (toExpr (0 : Int)) pow_pos)) |>.insert
             (mkApp3 (.const ``Int.emod_lt_of_pos []) x k pow_pos)
@@ -216,7 +216,7 @@ def analyzeAtom (e : Expr) : OmegaM (Std.HashSet Expr) := do
             (toExpr (0 : Nat)) b
           let pow_pos := mkApp3 (.const ``Nat.pos_pow_of_pos []) b exp (← mkDecideProof b_pos)
           let cast_pos := mkApp2 (.const ``Int.ofNat_pos_of_pos []) k' pow_pos
-          pure <| Std.HashSet.empty.insert
+          pure <| (∅ : Std.HashSet Expr).insert
             (mkApp3 (.const ``Int.emod_nonneg []) x k
                 (mkApp3 (.const ``Int.ne_of_gt []) k (toExpr (0 : Int)) cast_pos)) |>.insert
               (mkApp3 (.const ``Int.emod_lt_of_pos []) x k cast_pos)
@@ -224,18 +224,18 @@ def analyzeAtom (e : Expr) : OmegaM (Std.HashSet Expr) := do
         | (``Nat.cast, #[.const ``Int [], _, x']) =>
           -- Since we push coercions inside `%`, we need to record here that
           -- `(x : Int) % (y : Int)` is non-negative.
-          pure <| Std.HashSet.empty.insert (mkApp2 (.const ``Int.emod_ofNat_nonneg []) x' k)
+          pure <| (∅ : Std.HashSet Expr).insert (mkApp2 (.const ``Int.emod_ofNat_nonneg []) x' k)
         | _ => pure ∅
     | _ => pure ∅
   | (``Min.min, #[_, _, x, y]) =>
-    pure <| Std.HashSet.empty.insert (mkApp2 (.const ``Int.min_le_left []) x y) |>.insert
+    pure <| (∅ : Std.HashSet Expr).insert (mkApp2 (.const ``Int.min_le_left []) x y) |>.insert
       (mkApp2 (.const ``Int.min_le_right []) x y)
   | (``Max.max, #[_, _, x, y]) =>
-    pure <| Std.HashSet.empty.insert (mkApp2 (.const ``Int.le_max_left []) x y) |>.insert
+    pure <| (∅ : Std.HashSet Expr).insert (mkApp2 (.const ``Int.le_max_left []) x y) |>.insert
       (mkApp2 (.const ``Int.le_max_right []) x y)
   | (``ite, #[α, i, dec, t, e]) =>
       if α == (.const ``Int []) then
-        pure <| Std.HashSet.empty.insert <| mkApp5 (.const ``ite_disjunction [0]) α i dec t e
+        pure <| (∅ : Std.HashSet Expr).insert <| mkApp5 (.const ``ite_disjunction [0]) α i dec t e
       else
         pure {}
   | _ => pure ∅

src/Lean/Linter/UnusedVariables.lean

@@ -364,17 +364,17 @@ structure References where
   the spans for `foo`, `bar`, and `baz`. Global definitions are always treated as used.
   (It would be nice to be able to detect unused global definitions but this requires more
   information than the linter framework can provide.) -/
-  constDecls : Std.HashSet String.Range := .empty
+  constDecls : Std.HashSet String.Range := ∅
   /-- The collection of all local declarations, organized by the span of the declaration.
   We collapse all declarations declared at the same position into a single record using
   `FVarDefinition.aliases`. -/
-  fvarDefs : Std.HashMap String.Range FVarDefinition := .empty
+  fvarDefs : Std.HashMap String.Range FVarDefinition := ∅
   /-- The set of `FVarId`s that are used directly. These may or may not be aliases. -/
-  fvarUses : Std.HashSet FVarId := .empty
+  fvarUses : Std.HashSet FVarId := ∅
   /-- A mapping from alias to original FVarId. We don't guarantee that the value is not itself
   an alias, but we use `followAliases` when adding new elements to try to avoid long chains. -/
   -- TODO: use a `UnionFind` data structure here
-  fvarAliases : Std.HashMap FVarId FVarId := .empty
+  fvarAliases : Std.HashMap FVarId FVarId := ∅
   /-- Collection of all `MetavarContext`s following the execution of a tactic. We trawl these
   if needed to find additional `fvarUses`. -/
   assignments : Array (PersistentHashMap MVarId Expr) := #[]

src/Lean/Meta/Canonicalizer.lean

@@ -49,7 +49,7 @@ State for the `CanonM` monad.
 structure State where
   /-- Mapping from `Expr` to hash. -/
   -- We use `HashMap.Raw` to ensure we don't have to tag `State` as `unsafe`.
-  cache      : Std.HashMap.Raw ExprVisited UInt64 := Std.HashMap.Raw.empty
+  cache      : Std.HashMap.Raw ExprVisited UInt64 := ∅
   /--
   Given a hashcode `k` and `keyToExprs.find? h = some es`, we have that all `es` have hashcode `k`, and
   are not definitionally equal modulo the transparency setting used. -/

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

@@ -66,9 +66,9 @@ inductive PreExpr
 def toACExpr (op l r : Expr) : MetaM (Array Expr × ACExpr) := do
   let (preExpr, vars) ←
     toPreExpr (mkApp2 op l r)
-    |>.run Std.HashSet.empty
+    |>.run ∅
   let vars := vars.toArray.insertionSort Expr.lt
-  let varMap := vars.foldl (fun xs x => xs.insert x xs.size) Std.HashMap.empty |>.get!
+  let varMap := vars.foldl (fun xs x => xs.insert x xs.size) (∅ : Std.HashMap Expr Nat) |>.get!
 
   return (vars, toACExpr varMap preExpr)
   where

src/Lean/Server/References.lean

@@ -263,7 +263,7 @@ all identifiers that are being collapsed into one.
 -/
 partial def combineIdents (trees : Array InfoTree) (refs : Array Reference) : Array Reference := Id.run do
   -- Deduplicate definitions based on their exact range
-  let mut posMap : Std.HashMap Lsp.Range RefIdent := Std.HashMap.empty
+  let mut posMap : Std.HashMap Lsp.Range RefIdent := ∅
   for ref in refs do
     if let { ident, range, isBinder := true, .. } := ref then
       posMap := posMap.insert range ident
@@ -318,7 +318,7 @@ where
       canonicalRepresentative := idMap[canonicalRepresentative]
     return canonicalRepresentative
 
-  buildIdMap posMap := Id.run <| StateT.run' (s := Std.HashMap.empty) do
+  buildIdMap posMap := Id.run <| StateT.run' (s := ∅) do
     -- map fvar defs to overlapping fvar defs/uses
     for ref in refs do
       let baseId := ref.ident
@@ -348,7 +348,7 @@ are added to the `aliases` of the representative of the group.
 Yields to separate groups for declaration and usages if `allowSimultaneousBinderUse` is set.
 -/
 def dedupReferences (refs : Array Reference) (allowSimultaneousBinderUse := false) : Array Reference := Id.run do
-  let mut refsByIdAndRange : Std.HashMap (RefIdent × Option Bool × Lsp.Range) Reference := Std.HashMap.empty
+  let mut refsByIdAndRange : Std.HashMap (RefIdent × Option Bool × Lsp.Range) Reference := ∅
   for ref in refs do
     let isBinder := if allowSimultaneousBinderUse then some ref.isBinder else none
     let key := (ref.ident, isBinder, ref.range)

src/Lean/Util/Diff.lean

@@ -133,7 +133,7 @@ cautious when applying it to larger workloads.
 partial def lcs (left right : Subarray α) : Array α := Id.run do
   let (pref, left, right) := matchPrefix left right
   let (left, right, suff) := matchSuffix left right
-  let mut hist : Histogram α left.size right.size := .empty
+  let mut hist : Histogram α left.size right.size := (∅ : Std.HashMap ..)
   for h : i in [0:left.size] do
     hist := hist.addLeft ⟨i, Membership.get_elem_helper h rfl⟩ left[i]
   for h : i in [0:right.size] do

src/Lean/Util/HasConstCache.lean

@@ -10,7 +10,7 @@ import Std.Data.HashMap.Raw
 namespace Lean
 
 structure HasConstCache (declNames : Array Name) where
-  cache : Std.HashMap.Raw Expr Bool := Std.HashMap.Raw.empty
+  cache : Std.HashMap.Raw Expr Bool := ∅
 
 unsafe def HasConstCache.containsUnsafe (e : Expr) : StateM (HasConstCache declNames) Bool := do
   if let some r := (← get).cache.get? (beq := ⟨ptrEq⟩) e then

src/Lean/Util/MonadCache.lean

@@ -68,7 +68,7 @@ instance  : MonadHashMapCacheAdapter α β (MonadCacheT α β m) where
   modifyCache f := (modify f : StateRefT' ..)
 
 @[inline] def run {σ} (x : MonadCacheT α β m σ) : m σ :=
-  x.run' Std.HashMap.empty
+  x.run' ∅
 
 instance : Monad (MonadCacheT α β m) := inferInstanceAs (Monad (StateRefT' _ _ _))
 instance : MonadLift m (MonadCacheT α β m) := inferInstanceAs (MonadLift m (StateRefT' _ _ _))
@@ -92,7 +92,7 @@ instance  : MonadHashMapCacheAdapter α β (MonadStateCacheT α β m) where
   modifyCache f := (modify f : StateT ..)
 
 @[always_inline, inline] def run {σ} (x : MonadStateCacheT α β m σ) : m σ :=
-  x.run' Std.HashMap.empty
+  x.run' ∅
 
 instance : Monad (MonadStateCacheT α β m) := inferInstanceAs (Monad (StateT _ _))
 instance : MonadLift m (MonadStateCacheT α β m) := inferInstanceAs (MonadLift m (StateT _ _))

src/Lean/Util/SortExprs.lean

@@ -20,7 +20,7 @@ def sortExprs (es : Array Expr) (lt := true) : Array Expr × Perm :=
     es.qsort fun (e₁, _) (e₂, _) => e₁.lt e₂
   else
     es.qsort fun (e₁, _) (e₂, _) => e₂.lt e₁
-  let (_, perm) := es.foldl (init := (0, Std.HashMap.empty)) fun (i, perm) (_, j) => (i+1, perm.insert j i)
+  let (_, perm) := es.foldl (init := (0, ∅)) fun (i, perm) (_, j) => (i+1, perm.insert j i)
   let es := es.map (·.1)
   (es, perm)
 

src/Std/Sat/AIG/Basic.lean

@@ -293,7 +293,7 @@ Transform an `Entrypoint` into a graphviz string. Useful for debugging purposes.
 def toGraphviz {α : Type} [DecidableEq α] [ToString α] [Hashable α] (entry : Entrypoint α) :
     String :=
   let ⟨⟨decls, _, hinv⟩, ⟨idx, h⟩⟩ := entry
-  let (dag, s) := go "" decls hinv idx h |>.run .empty
+  let (dag, s) := go "" decls hinv idx h |>.run ∅
   let nodes := s.fold (fun x y ↦ x ++ toGraphvizString decls y) ""
   "Digraph AIG {" ++ nodes ++ dag ++ "}"
 where

src/lake/Lake/Config/Module.lean

@@ -30,7 +30,7 @@ instance : Hashable Module where hash m := hash m.keyName
 instance : BEq Module where beq m n := m.keyName == n.keyName
 
 abbrev ModuleSet := Std.HashSet Module
-@[inline] def ModuleSet.empty : ModuleSet := Std.HashSet.empty
+@[inline] def ModuleSet.empty : ModuleSet := ∅
 
 abbrev OrdModuleSet := OrdHashSet Module
 @[inline] def OrdModuleSet.empty : OrdModuleSet := OrdHashSet.empty

src/lake/Lake/Config/Package.lean

@@ -422,7 +422,7 @@ instance : Hashable Package where hash pkg := hash pkg.config.name
 instance : BEq Package where beq p1 p2 := p1.config.name == p2.config.name
 
 abbrev PackageSet := Std.HashSet Package
-@[inline] def PackageSet.empty : PackageSet := Std.HashSet.empty
+@[inline] def PackageSet.empty : PackageSet := ∅
 
 abbrev OrdPackageSet := OrdHashSet Package
 @[inline] def OrdPackageSet.empty : OrdPackageSet := OrdHashSet.empty

src/lake/Lake/Util/OrdHashSet.lean

@@ -22,12 +22,12 @@ variable [Hashable α] [BEq α]
 instance : Coe (OrdHashSet α) (Std.HashSet α) := ⟨toHashSet⟩
 
 def empty : OrdHashSet α :=
-  ⟨.empty, .empty⟩
+  ⟨∅, .empty⟩
 
 instance : EmptyCollection (OrdHashSet α) := ⟨empty⟩
 
 def mkEmpty (size : Nat) : OrdHashSet α :=
-  ⟨.empty, .mkEmpty size⟩
+  ⟨∅, .mkEmpty size⟩
 
 def insert (self : OrdHashSet α) (a : α) : OrdHashSet α :=
   if self.toHashSet.contains a then