Documentation

Lean.Meta.Tactic.Injection

Equations
    Instances For
      Instances For
        Equations
          Instances For
            Instances For
              def Lean.Meta.injectionIntro (mvarId : MVarId) (numEqs : Nat) (newNames : List Name) (tryToClear : Bool := true) :
              Equations
                Instances For
                  Equations
                    Instances For
                      def Lean.Meta.injection (mvarId : MVarId) (fvarId : FVarId) (newNames : List Name := []) :
                      Equations
                        Instances For
                          • solved : InjectionsResult

                            injections closed the input goal.

                          • subgoal (mvarId : MVarId) (remainingNames : List Name) (forbidden : FVarIdSet) : InjectionsResult

                            injections produces a new goal mvarId. remainingNames contains the user-facing names that have not been used. forbidden contains all local declarations to which injection has been applied. Recall that some of these declarations may not have been eliminated from the local context due to forward dependencies, and we use forbidden to avoid non-termination when using injections in a loop.

                          Instances For
                            def Lean.Meta.injections (mvarId : MVarId) (newNames : List Name := []) (maxDepth : Nat := 5) (forbidden : FVarIdSet := ) :

                            Applies injection to local declarations in mvarId. It uses newNames to name the new local declarations. maxDepth is the maximum recursion depth. Only local declarations that are not in forbidden are considered. Recall that some of local declarations may not have been eliminated from the local context due to forward dependencies, and we use forbidden to avoid non-termination when using injections in a loop.

                            Equations
                              Instances For
                                partial def Lean.Meta.injections.go (depth : Nat) (fvarIds : List FVarId) (mvarId : MVarId) (newNames : List Name) (forbidden : FVarIdSet) :