Lean4
/-- * `constructorm p_1, ..., p_n` applies the `constructor` tactic to the main goal
if `type` matches one of the given patterns.
* `constructorm* p` is a more efficient and compact version of `· repeat constructorm p`.
It is more efficient because the pattern is compiled once.
Example: The following tactic proves any theorem like `True ∧ (True ∨ True)` consisting of
and/or/true:
```
constructorm* _ ∨ _, _ ∧ _, True
```
-/
@[tactic_parser 1000]
public meta def constructorM : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.constructorM 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "constructorm" false✝)
(ParserDescr.unary✝ `optional (ParserDescr.symbol✝ "*")))
(ParserDescr.unary✝ `group (ParserDescr.const✝ `ppSpace)))
((with_annotate_term"sepBy1(" @ParserDescr.sepBy1✝) (ParserDescr.cat✝ `term 0) "," (ParserDescr.symbol✝ ", ")
Bool.false✝))
