Equations
- tacticSimp_wf = Lean.ParserDescr.node `tacticSimp_wf 1024 (Lean.ParserDescr.nonReservedSymbol "simp_wf" false)
Equations
- tacticDecreasing_trivial = Lean.ParserDescr.node `tacticDecreasing_trivial 1024 (Lean.ParserDescr.nonReservedSymbol "decreasing_trivial" false)
Equations
- tacticDecreasing_with_ = Lean.ParserDescr.node `tacticDecreasing_with_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "decreasing_with " false) (Lean.ParserDescr.const `tacticSeq))
Equations
- tacticDecreasing_tactic = Lean.ParserDescr.node `tacticDecreasing_tactic 1024 (Lean.ParserDescr.nonReservedSymbol "decreasing_tactic" false)