Is there a NOOP in Lean?

Stream: new members

[Anders Larsson]

A beginner question here, how do I deal with side effects in a match statement where the default is to not update anything?

inductive Days where
| monday
| tuesday
| saturday
| someOtherDay

def processDay (day: Days): StateM Nat Unit := do
  match day with
  | .monday => set ((← get) + 1)
  | .saturday => set 3
  | _ => let _ := 999999   -- Is must be a prettier way to do this?

#eval processDay .saturday 0 -- ((), 3)

[Kyle Miller]

def processDay (day: Days): StateM Nat Unit := do
  match day with
  | .monday => set ((← get) + 1)
  | .saturday => set 3
  | _ => pure ()

[Kyle Miller]

You have to be careful since return can be used for early returns, but in a do block you can use return instead of pure ().

[Anders Larsson]

Thank you,
I didn't realize that pure and return differed in that way.