Convert Monads to Units

Stream: lean4

[Gareth Ma]

Hi, is there a function that turns a TacticM Bool to a TacticM Unit?

[Gareth Ma]

Something that behaves like do let _ ← tactic ; return

[Adam Topaz]

I think there's something called docs#discard ? (modulo namespaces)

[Gareth Ma]

Ah yes

[Gareth Ma]

Thanks!!

[Adam Topaz]

In case anyone else is looking, it's docs#Functor.discard