Documentation

Lean.Meta.Tactic.Injection

source
def Lean.Meta.getCtorNumPropFields (ctorInfo : Lean.ConstructorVal) :
Lean.MetaM Nat
Equations
  • One or more equations did not get rendered due to their size.
source
inductive Lean.Meta.InjectionResultCore :
Type
Instances For
    source
    def Lean.Meta.injectionCore (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) :
    Lean.MetaM Lean.Meta.InjectionResultCore
    Equations
    • One or more equations did not get rendered due to their size.
    source
    inductive Lean.Meta.InjectionResult :
    Type
    Instances For
      source
      def Lean.Meta.injectionIntro (mvarId : Lean.MVarId) (numEqs : Nat) (newNames : List Lean.Name) (tryToClear : optParam Bool true) :
      Lean.MetaM Lean.Meta.InjectionResult
      Equations
      source
      def Lean.Meta.injectionIntro.go (tryToClear : optParam Bool true) :
      Nat → Lean.MVarId → Array Lean.FVarId → List Lean.Name → Lean.MetaM Lean.Meta.InjectionResult
      Equations
      source
      def Lean.Meta.injection (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (newNames : optParam (List Lean.Name) []) :
      Lean.MetaM Lean.Meta.InjectionResult
      Equations
      • One or more equations did not get rendered due to their size.
      source
      inductive Lean.Meta.InjectionsResult :
      Type
      Instances For
        source
        def Lean.Meta.injections (mvarId : Lean.MVarId) (newNames : optParam (List Lean.Name) []) (maxDepth : optParam Nat 5) :
        Lean.MetaM Lean.Meta.InjectionsResult
        Equations
        • One or more equations did not get rendered due to their size.
        source
        partial def Lean.Meta.injections.go (mvarId : Lean.MVarId) :
        Nat → List Lean.FVarId → Lean.MVarId → List Lean.Name → Lean.MetaM Lean.Meta.InjectionsResult