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.

      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
            def Lean.Elab.Tactic.ElimApp.evalAlts (elimInfo : Lean.Meta.ElimInfo) (alts : Array Lean.Elab.Tactic.ElimApp.Alt) (optPreTac : Lean.Syntax) (altStxs : Array Lean.Syntax) (initialInfo : Lean.Elab.Info) (numEqs : optParam Nat 0) (numGeneralized : optParam Nat 0) (toClear : optParam (Array Lean.FVarId) #[]) (toTag : optParam (Array (Lean.Ident × 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

                  Applies syntactic alternative to alternative goal.

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

                    Applies induction .. with $preTac | .., if any, to an alternative goal.

                    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