Documentation

Lean.Elab.Tactic.Induction

Equations
Instances For
    Equations
    • One or more equations did not get rendered due to their size.
    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

      • 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
        Equations

        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.

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

          Given a goal ... targets ... |- C[targets] associated with mvarId, assign motiveArg := fun targets => C[targets]

          Equations
          • One or more equations did not get rendered due to their size.
          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.

            Equations
            • One or more equations did not get rendered due to their size.
            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) #[]) :
              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
                        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