This repository was archived by the owner on Jul 24, 2024. It is now read-only.
This repository was archived by the owner on Jul 24, 2024. It is now read-only.
The rcases params aren't printed right by lean #1090
Description
As pointed out by Kevin, if you mouse over rcases inside a begin ... end block you are greeted with the lovely
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)>I wonder how small the hoop we have to jump through in order to fix is.