Documentation

Lean.Meta.Tactic.Grind.Split

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

Selects a case-split from the list of candidates, and adds new choice point (aka backtracking point). Returns true if successful.

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