Instances For
Helper method for creating an user-defined eliminator/recursor application.
- name : Lake.Name
The short name of the alternative, used in
| foo =>cases A declaration corresponding to the inductive constructor. (For custom recursors, the alternatives correspond to parameter names in the recursor, so we may not have a declaration to point to.) This is used for go-to-definition on the alternative name.
- mvarId : Lean.MVarId
The subgoal metavariable for the alternative.
Instances For
- elimInfo : Lean.Meta.ElimInfo
Instances For
Instances For
- elimApp : Lean.Expr
- others : Array Lean.MVarId
Instances For
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.
Instances For
Given a goal ... targets ... |- C[targets] associated with mvarId, assign
motiveArg := fun targets => C[targets]
Instances For
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.