Documentation

Lean.Meta.Tactic.SplitIf

@[reducible, inline]

Return an if-then-else or match-expr to split.

Equations

Default Simp.Context for simpIf methods. It contains all congruence theorems, but just the rewriting rules for reducing if expressions.

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