def elabGrindCases : Lean.Elab.Tactic.TacticM Unit

Equations

• One or more equations did not get rendered due to their size.

def tacticGrind_cases : Lean.ParserDescr

Looks at the case l label of each goal and tries to solve it by grind [Foo.l] where Foo is the head of the goal type, possibly under a telescope of universal quantifiers.

Equations

• tacticGrind_cases = Lean.ParserDescr.node `tacticGrind_cases 1024 (Lean.ParserDescr.nonReservedSymbol "grind_cases" false)