Structure representing a tactic which can be used by tactic.auto_cases.
The auto_cases_tac for tactic.cases.
The auto_cases_tac for tactic.induction.
Find an auto_cases_tac which matches the given type : expr.
meta
def
tactic.auto_cases_at
(find : expr → option tactic.auto_cases.auto_cases_tac)
(hyp : expr) :
Applies cases or induction on the local_hypothesis hyp : expr.
meta
def
tactic.auto_cases
(find : expr → option tactic.auto_cases.auto_cases_tac := tactic.auto_cases.find_tac) :
Applies cases or induction on certain hypotheses.