fix(init/meta/interactive_base): add missing parser_desc combinators (#…

…676)

Add some missing combinators that were unearthed when switching on the unprintable tactic linter leanprover-community/mathlib3#11725 .

library/init/meta/interactive_base.lean

@@ -110,6 +110,7 @@ private meta def parser_desc_aux : expr → tactic (list format)
 | `(pure ._) := return []
 | `(._ <$> %%p) := parser_desc_aux p
 | `(skip_info %%p) := parser_desc_aux p
+| `(._ <$ %%p) := parser_desc_aux p
 | `(set_goal_info_pos %%p) := parser_desc_aux p
 | `(with_desc %%desc %%p) := list.ret <$> eval_expr format desc
 | `(%%p₁ <*> %%p₂) := do
@@ -124,6 +125,10 @@ private meta def parser_desc_aux : expr → tactic (list format)
   f₁ ← parser_desc_aux p₁,
   f₂ ← parser_desc_aux p₂,
   return $ concat f₁ f₂
+| `(%%p₁ >> %%p₂) := do
+  f₁ ← parser_desc_aux p₁,
+  f₂ ← parser_desc_aux p₂,
+  return $ concat f₁ f₂
 | `(many %%p) := do
   f ← parser_desc_aux p,
   return [maybe_paren f ++ "*"]