looping over hashmap runs into error

Stream: new members

[Alok Singh]

/-- The Levi Civita Field -/
structure LeviCivita where
  /-- repr as rationals -/
  coeffs : Std.HashMap Rat Rat
deriving Repr

#eval (LeviCivita.mk (Std.HashMap.empty.insert 1 2) : LeviCivita)

deriving instance Hashable for Rat

def LeviCivita.add (a: LeviCivita) (b: LeviCivita) : LeviCivita:= Id.run do
    let mut out: Std.HashMap Rat Rat := Std.HashMap.empty
    for (pwr, coeff) in a.coeffs do
      if b.coeffs.contains pwr then
        let coeff' := a.coeffs[pwr]+b.coeffs[pwr]
      else
        let coeff' := a.coeffs[pwr] + 0
      out := out.insert pwr (coeff')
    ⟨out⟩

leads to this issue
2024-01-15-18-47-09.png

I really have no idea why looping is failing

[Matt Diamond]

maybe Std.HashMap doesn't have a ForIn instance?

[Matt Diamond]

you could import Std.Lean.HashMap and use Lean.HashMap instead... that one has a ForIn instance

[Matt Diamond]

btw, if you're trying to do pointwise addition on the two HashMaps, I don't think you even need the for loop... you can just do this:

def LeviCivita.add (a: LeviCivita) (b: LeviCivita) : LeviCivita :=
⟨a.coeffs.mergeWith (fun _ c1 c2 => c1 + c2) b.coeffs⟩

[Alok Singh]

ah, hadn't realized there were 2 and i used the other

[Alok Singh]

in a related vein, this made me wonder about notation like #{a => b} for hashmaps.