Helper method for creating an user-defined eliminator/recursor application.

  • name : Lake.Name

    The short name of the alternative, used in | foo => cases

  • declName? : Option Lake.Name

    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
    @[inline, reducible]
    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
              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.

          Instances For
            def Lean.Elab.Tactic.ElimApp.evalAlts (elimInfo : Lean.Meta.ElimInfo) (alts : Array Lean.Elab.Tactic.ElimApp.Alt) (optPreTac : Lean.Syntax) (altsSyntax : Array Lean.Syntax) (initialInfo : Lean.Elab.Info) (numEqs : optParam Nat 0) (numGeneralized : optParam Nat 0) (toClear : optParam (Array Lean.FVarId) #[]) :
            Instances For
              Instances For