Documentation

Construct the an eliminator/recursor application. targets contains the explicit and implicit targets for the eliminator. For example, the indices of builtin recursors are considered implicit targets. Remark: the method addImplicitTargets may be used to compute the sequence of implicit and explicit targets from the explicit ones.

If altsSyntax is not empty we reorder alts using the order the alternatives have been provided in altsSyntax. Motivations:

1- It improves the effectiveness of the checkpoint and save tactics. Consider the following example:

example (h₁ : p ∨ q) (h₂ : p → x = 0) (h₃ : q → y = 0) : x * y = 0 := by
  cases h₁ with
  | inr h =>
    sleep 5000 -- sleeps for 5 seconds
    save
    have : y = 0 := h₃ h
    -- We can confortably work here
  | inl h => stop ...

If we do reorder, the inl alternative will be executed first. Moreover, as we type in the inr alternative, type errors will "swallow" the inl alternative and affect the tactic state at save making it ineffective.

2- The errors are produced in the same order the appear in the code above. This is not super important when using IDEs.