def tacticSimp_currInstr : Lean.ParserDescr

def tacticSimp_t_update : Lean.ParserDescr

def tacticZero_lt_ne_zero : Lean.ParserDescr

def tacticHoare_simp_specification : Lean.ParserDescr

def tacticSimp_jump_spec_false : Lean.ParserDescr

def tacticSimp_jump_spec_true : Lean.ParserDescr

def tacticSimp_jump_spec : Lean.ParserDescr

def tacticAutoSeq : Lean.ParserDescr

def «tacticSapply_s_seq_,_,_,_» : Lean.ParserDescr

def «tacticSapply_s_seq'_,_,_,_» : Lean.ParserDescr

def «tacticSapply_s_seq''_,_,_,_,_» : Lean.ParserDescr

def «tacticSapply_s_seq''R:=_,L_W:=_,L_W':=_,L_B:=_,L_B':=_» : Lean.ParserDescr

def «tacticSapply_s_seq''P:=_,R:=_,L_W:=_,L_W':=_,L_B:=_,L_B':=_» : Lean.ParserDescr

def «tacticSapply_s_seq_plainP:=_,R:=_,L_W:=_,L_W':=_,L_B:=_,L_B':=_» : Lean.ParserDescr

def «tacticSapply_s_seq_plainR:=_,L_W:=_,L_W':=_,L_B:=_,L_B':=_» : Lean.ParserDescr

def «tacticSapply_s_seq'''P:=_,R:=_,L_W:=_,L_W':=_,L_B:=_,L_B':=_» : Lean.ParserDescr

def «tacticSapply_s_seq'''R:=_,L_W:=_,L_W':=_,L_B:=_,L_B':=_» : Lean.ParserDescr

def tacticPrepare_second_seq : Lean.ParserDescr

def tacticApply_spec_basic_ : Lean.ParserDescr

def tacticApply_spec_when_ready_ : Lean.ParserDescr

def RCasesPatt.alts' (ref : Lean.Syntax) : List Lean.Elab.Tactic.RCases.RCasesPatt → Lean.Elab.Tactic.RCases.RCasesPatt

partial def RCasesPatt.parse (stx : Lean.Syntax) : Lean.MetaM Lean.Elab.Tactic.RCases.RCasesPatt

Parses a Syntax into the RCasesPatt type used by the RCases tactic.

def tacticSplit_condisIn_ : Lean.ParserDescr

def tacticApply_spec_default_ : Lean.ParserDescr

def tacticApply_spec_for_second_ : Lean.ParserDescr

def tacticApply_spec_ : Lean.ParserDescr