Documentation

Lean.Elab.Tactic.Do.ProofMode.Focus

source
structure Lean.Elab.Tactic.Do.ProofMode.FocusResult :
Type

The result of focussing the context of a goal goal : MGoal on a particular hypothesis. The focussed hypothesis is returned as focusHyp : Expr, along with the residual restHyps : Expr and a proof : Expr for the property goal.hyps ⊣⊢ₛ restHyps ∧ focusHyp.

Instances For
    source
    instance Lean.Elab.Tactic.Do.ProofMode.instInhabitedFocusResult :
    Inhabited FocusResult
    Equations
      source
      partial def Lean.Elab.Tactic.Do.ProofMode.focusHyp (σs e : Expr) (name : Name) :
      Option FocusResult
      source
      def Lean.Elab.Tactic.Do.ProofMode.MGoal.focusHyp (goal : MGoal) (name : Name) :
      Option FocusResult
      Equations
        Instances For
          source
          def Lean.Elab.Tactic.Do.ProofMode.FocusResult.refl (σs restHyps focusHyp : Expr) :
          FocusResult
          Equations
            Instances For
              source
              def Lean.Elab.Tactic.Do.ProofMode.FocusResult.restGoal (res : FocusResult) (goal : MGoal) :
              MGoal
              Equations
                Instances For
                  source
                  def Lean.Elab.Tactic.Do.ProofMode.FocusResult.recombineGoal (res : FocusResult) (goal : MGoal) :
                  MGoal
                  Equations
                    Instances For
                      source
                      def Lean.Elab.Tactic.Do.ProofMode.FocusResult.rewriteHyps (res : FocusResult) (goal : MGoal) :
                      Expr → Expr

                      Turn a proof for (res.recombineGoal goal).toExpr into one for goal.toExpr.

                      Equations
                        Instances For
                          source
                          def Lean.Elab.Tactic.Do.ProofMode.MGoal.focusHypWithInfo (goal : MGoal) (name : Ident) :
                          MetaM FocusResult
                          Equations
                            Instances For