Documentation

Lean.Meta.Tactic.FunIndInfo

This module defines the data structure and environment extension to remember how to map the function's arguments to the functional induction principle's arguments. Also used for functional cases.

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

    A FunIndInfo indicates how a function's arguments map to the arguments of the functional induction (resp. cases) theorem.

    The size of params also indicates the arity of the function.

    • funName : Name
    • funIndName : Name
    • levelMask : Array Bool

      true means that the corresponding level parameter of the function is also a level param of the induction principle.

    Instances For
      Equations
      Instances For
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          def Lean.Meta.getFunInductName (declName : Name) (unfolding : Bool := false) :
          Equations
          Instances For
            def Lean.Meta.getFunCasesName (declName : Name) (unfolding : Bool := false) :
            Equations
            Instances For
              def Lean.Meta.getMutualInductName (declName : Name) (unfolding : Bool := false) :
              Equations
              Instances For
                def Lean.Meta.getFunInduct? (unfolding cases : Bool) (declName : Name) :
                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
                    Instances For
                      def Lean.Meta.getFunIndInfo? (cases unfolding : Bool) (funName : Name) :
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For