def tacticSimp_schedule1 : Lean.ParserDescr

Equations

• tacticSimp_schedule1 = Lean.ParserDescr.node `tacticSimp_schedule1 1024 (Lean.ParserDescr.nonReservedSymbol "simp_schedule1" false)

def tacticSimp_schedule2 : Lean.ParserDescr

Equations

• tacticSimp_schedule2 = Lean.ParserDescr.node `tacticSimp_schedule2 1024 (Lean.ParserDescr.nonReservedSymbol "simp_schedule2" false)

def tacticSimp_flag : Lean.ParserDescr

Equations

• tacticSimp_flag = Lean.ParserDescr.node `tacticSimp_flag 1024 (Lean.ParserDescr.nonReservedSymbol "simp_flag" false)