StateM and discard operator

Stream: new members

[Mark R. Tuttle]

Is there a discard >> variant of >>= for StateM monads?

In the following example, the use of >> fails with the error message "Failed to synthesize HAndThen". I'm not sure how to answer the question on my own. I tried searching for "discard" in the top-level documentation and github.

structure State where
  a: Nat
  b: Nat

def State.update_a: StateM State Unit := do
  let state ← get
  set {state with a := state.a + 1}

def State.update_b: StateM State Unit := do
  let state ← get
  set {state with b := state.b + 1}

def State.update: StateM State Unit := do
  State.update_a >> State.update_b

[Matthew Ballard]

You might have better luck with https://leanprover-community.github.io/mathlib4_docs