mathlib3 documentation

tactic.split_ifs

source
meta def tactic.find_if_cond  :
expr → option expr
source
meta def tactic.find_if_cond_at (at_ : interactive.loc) :
tactic (option expr)
source
meta def tactic.reduce_ifs_at (at_ : interactive.loc) :
tactic unit
source
meta def tactic.split_if1 (c : expr) (n : name) (at_ : interactive.loc) :
tactic unit
source
meta def tactic.split_ifs (names : list name) (at_ : interactive.loc := interactive.loc.ns [option.none]) :
tactic unit
source
meta def tactic.interactive.split_ifs (at_ : interactive.parse interactive.types.location) (names : interactive.parse interactive.types.with_ident_list) :
tactic unit

Splits all if-then-else-expressions into multiple goals.

Given a goal of the form g (if p then x else y), split_ifs will produce two goals: p ⊢ g x and ¬p ⊢ g y.

If there are multiple ite-expressions, then split_ifs will split them all, starting with a top-most one whose condition does not contain another ite-expression.

split_ifs at * splits all ite-expressions in all hypotheses as well as the goal.

split_ifs with h₁ h₂ h₃ overrides the default names for the hypotheses.

source
def tactic_doc.tactic.split_ifs  :
tactic_doc_entry

Splits all if-then-else-expressions into multiple goals.

Given a goal of the form g (if p then x else y), split_ifs will produce two goals: p ⊢ g x and ¬p ⊢ g y.

If there are multiple ite-expressions, then split_ifs will split them all, starting with a top-most one whose condition does not contain another ite-expression.

split_ifs at * splits all ite-expressions in all hypotheses as well as the goal.

split_ifs with h₁ h₂ h₃ overrides the default names for the hypotheses.