HepLean 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.
Instances For
    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.
      Instances For
        source
        inductive Lean.Meta.InjectionResult :
        Type
        Instances For
          source
          def Lean.Meta.injectionIntro (mvarId : Lean.MVarId) (numEqs : Nat) (newNames : List Lake.Name) (tryToClear : optParam Bool true) :
          Lean.MetaM Lean.Meta.InjectionResult
          Equations
          Instances For
            source
            def Lean.Meta.injectionIntro.go (tryToClear : optParam Bool true) :
            Nat → Lean.MVarId → Array Lean.FVarId → List Lake.Name → Lean.MetaM Lean.Meta.InjectionResult
            Equations
            Instances For
              source
              def Lean.Meta.injection (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (newNames : optParam (List Lake.Name) []) :
              Lean.MetaM Lean.Meta.InjectionResult
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                inductive Lean.Meta.InjectionsResult :
                Type
                Instances For
                  source
                  def Lean.Meta.injections (mvarId : Lean.MVarId) (newNames : optParam (List Lake.Name) []) (maxDepth : optParam Nat 5) :
                  Lean.MetaM Lean.Meta.InjectionsResult
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    partial def Lean.Meta.injections.go (mvarId : Lean.MVarId) :
                    Nat → List Lean.FVarId → Lean.MVarId → List Lake.Name → Lean.MetaM Lean.Meta.InjectionsResult