Documentation

Lean.Meta.Tactic.Induction

Equations
Instances For
    Equations
    def Lean.Meta.getMajorTypeIndices (mvarId : Lean.MVarId) (tacticName : Lake.Name) (recursorInfo : Lean.Meta.RecursorInfo) (majorType : Lean.Expr) :

    Auxiliary method for implementing induction-like tactics. It retrieves indices from majorType using recursorInfo. Remark: mvarId and tacticName are used to generate error messages.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      def Lean.Meta.mkRecursorAppPrefix (mvarId : Lean.MVarId) (tacticName : Lake.Name) (majorFVarId : Lean.FVarId) (recursorInfo : Lean.Meta.RecursorInfo) (indices : Array Lean.Expr) :

      Auxiliary method for implementing induction-like tactics. It creates the prefix of a recursor application up-to motive. The motive is computed by abstracting major and indices at mvarId.getType. It retrieves indices from majorType using recursorInfo. Remark: mvarId and tacticName are used to generate error messages.

      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
          @[deprecated Lean.MVarId.induction]
          Equations
          • Lean.Meta.induction mvarId majorFVarId recursorName givenNames = mvarId.induction majorFVarId recursorName givenNames
          Instances For