rcases <error while executing interactive.param_desc: don't know how to pretty print
[has_bind.bind (monad.to_has_bind lean.parser)] (optional (tk "?")) (λ (hint : option unit), texpr >>=
λ (p : pexpr), (λ (_a : option unit), option.cases_on _a (id_rhs (lean.parser (pexpr × (list_Sigma (list_Pi rcases_patt) ⊕ ℕ)))
(optional (tk "with" *> rcases_patt_parse_list) >>= λ (ids : option (list_Sigma rcases_patt_inverted)), pure (p, sum.inl (rcases_patt_inverted.invert_list (option.get_or_else ids [default rcases_patt_inverted])))))
(λ (val : unit), id_rhs (lean.parser (pexpr × (list_Sigma (list_Pi rcases_patt) ⊕ ℕ)))
(rcases_parse_depth >>= λ (depth : ℕ), pure (p, sum.inr depth)))) hint)>