Documentation

Lean.Meta.Tactic.FunIndCollect

Support for collecting function calls that could be used for fun_induction or fun_cases. Used by fun_induction foo, and the Calls structure is also used by try?.

Instances For
    Instances For
      Equations
        Instances For
          def Lean.Meta.FunInd.SeenCalls.push (e : Expr) (funIndInfo : FunIndInfo) (args : Array Expr) (calls : SeenCalls) :
          Equations
            Instances For

              Which functions have exactly one candidate application. Used by try? to determine whether we can use fun_induction foo or need fun_induction foo x y z.

              Equations
                Instances For
                  @[reducible, inline]
                  Equations
                    Instances For
                      Equations
                        Instances For
                          Equations
                            Instances For
                              @[reducible, inline]
                              Equations
                                Instances For
                                  unsafe def Lean.Meta.FunInd.Collector.main (needle : FunIndInfo) (mvarId : MVarId) :
                                  Equations
                                    Instances For
                                      Equations
                                        Instances For