Documentation

Lean.Meta.Tactic.SplitIf

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

Equations
Instances For

    Default discharge? function for simpIf methods. It only uses hypotheses from the local context. It is effective after a case-split.

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

      Return the condition of an if expression to case split.

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