Basic Operations🔗

To use HashMap, you usually need to provide types for keys and values. The key type must have Hashable and BEq instances.

def myMap : HashMap String Nat := {}

-- Inserting values
def updatedMap := myMap.insert "apple" 1
def updatedMap2 := updatedMap.insert "banana" 2

-- Accessing values (returns Option)
some 1#eval updatedMap2.get? "apple" 
none#eval updatedMap2.get? "cherry"

-- Checking for existence
true#eval updatedMap2.contains "apple"

-- Removing values
def erasedMap := updatedMap2.erase "apple"
false#eval erasedMap.contains "apple"

-- Updating values using 'alter'
/-- Increment the value for a key, or initialize it to 1 -/
def increment (map : HashMap String Nat) (key : String)
  : HashMap String Nat :=
  map.alter key fun
    | some n => some (n + 1)
    | none   => some 1

some 2#eval (increment updatedMap2 "apple").get? "apple"