doc-string bug?

Stream: general

[Manuel Candales]

This is what I see when I clic on "set".
set !? id <error while executing interactive.param_desc: don't know how to pretty print [has_bind.bind monad.to_has_bind] (lean.parser.tk ":") (λ (_x : unit), interactive.types.texpr)> := expr <error while executing interactive.param_desc: don't know how to pretty print [has_bind.bind monad.to_has_bind] (lean.parser.tk "with") (λ (_x : unit), optional (lean.parser.tk "<-") >>= λ (arrow : option unit), lean.parser.ident >>= λ (h : name), return ↑(arrow.is_some, h))>

[Eric Wieser]

I assume you mean docs#tactic.interactive.set as opposed to docs#set?

[Manuel Candales]

yes, the tactic.