mathlib documentation

tactic.auto_cases

source
meta structure tactic.auto_cases.auto_cases_tac  :
Type 1

Structure representing a tactic which can be used by tactic.auto_cases.

source
meta def tactic.auto_cases.tac_cases  :
tactic.auto_cases.auto_cases_tac

The auto_cases_tac for tactic.cases.

source
meta def tactic.auto_cases.tac_induction  :
tactic.auto_cases.auto_cases_tac

The auto_cases_tac for tactic.induction.

source
meta def tactic.auto_cases.find_tac  :
expr → option tactic.auto_cases.auto_cases_tac

Find an auto_cases_tac which matches the given type : expr.

source
meta def tactic.auto_cases_at (hyp : expr) :
tactic string

Applies cases or induction on the local_hypothesis hyp : expr.

source
meta def tactic.auto_cases  :
tactic string

Applies cases or induction on certain hypotheses.