Documentation

Lean.Elab.Tactic.Do.ProofMode.Pure

source
def Lean.Elab.Tactic.Do.ProofMode.mPureCore {m : Type → Type u_1} {α : Type} [Monad m] [MonadControlT MetaM m] [MonadLiftT MetaM m] (σs hyp : Expr) (name : TSyntax `Lean.binderIdent) (k : Expr → Expr → m (α × MGoal × Expr)) :
m (α × MGoal × Expr)
Instances For
    source
    def Lean.Elab.Tactic.Do.ProofMode.elabMPure :
    Tactic
    Instances For
      source
      def Lean.Elab.Tactic.Do.ProofMode.mPureIntroCore {m : Type → Type u_1} {α : Type} [Monad m] [MonadLiftT MetaM m] (goal : MGoal) (k : Expr → m (α × Expr)) :
      m (α × Expr)
      Instances For
        source
        def Lean.Elab.Tactic.Do.ProofMode.elabMPureIntro :
        Tactic
        Instances For
          source
          partial def Lean.MVarId.applyRflAndAndIntro (mvar : MVarId) :
          MetaM Unit
          source
          def Lean.Elab.Tactic.Do.ProofMode.MGoal.pureRflAndAndIntro (goal : MGoal) :
          OptionT MetaM Expr
          Instances For
            source
            def Lean.Elab.Tactic.Do.ProofMode.MGoal.pureTrivial (goal : MGoal) :
            OptionT MetaM Expr
            Instances For