Documentation

Lean.Elab.Tactic.Do.ProofMode.Focus

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

The result of focusing the context of a goal goal : MGoal on a particular hypothesis. The focused 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
    def Lean.Elab.Tactic.Do.ProofMode.instInhabitedFocusResult.default :
    FocusResult
    Instances For
      source
      @[implicit_reducible]
      instance Lean.Elab.Tactic.Do.ProofMode.instInhabitedFocusResult :
      Inhabited FocusResult
      source
      partial def Lean.Elab.Tactic.Do.ProofMode.focusHyp (u : Level) (σs e : Expr) (name : Name) :
      Option FocusResult
      source
      def Lean.Elab.Tactic.Do.ProofMode.MGoal.focusHyp (goal : MGoal) (name : Name) :
      Option FocusResult
      Instances For
        source
        def Lean.Elab.Tactic.Do.ProofMode.FocusResult.refl (u : Level) (σs restHyps focusHyp : Expr) :
        FocusResult
        Instances For
          source
          def Lean.Elab.Tactic.Do.ProofMode.FocusResult.restGoal (res : FocusResult) (goal : MGoal) :
          MGoal
          Instances For
            source
            def Lean.Elab.Tactic.Do.ProofMode.FocusResult.recombineGoal (res : FocusResult) (goal : MGoal) :
            MGoal
            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.

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