1  -- examples/lean/HashMap.lean
 2  -- Test using Std.HashMap from Lean's standard library
 3  
 4  import Std.Data.HashMap
 5  
 6  def main : IO Unit := do
 7    let mut map : Std.HashMap String Nat := {}
 8    map := map.insert "straylight" 2026
 9    map := map.insert "aleph" 42
10    IO.println s!"HashMap test: {map.size} entries"
11    IO.println s!"straylight = {map["straylight"]?}"