def Lean.Elab.Tactic.Do.ProofMode.patAsTerm (pat : Parser.Tactic.MRefinePat) (expected : Option Expr := none) : OptionT TacticM Expr

Equations

• One or more equations did not get rendered due to their size.
• Lean.Elab.Tactic.Do.ProofMode.patAsTerm (Lean.Parser.Tactic.MRefinePat.pure t) expected = liftM (Lean.Elab.Tactic.elabTerm t.raw expected)
• Lean.Elab.Tactic.Do.ProofMode.patAsTerm pat expected = failure

partial def Lean.Elab.Tactic.Do.ProofMode.mRefineCore (goal : MGoal) (pat : Parser.Tactic.MRefinePat) (k : MGoal → TSyntax `Lean.binderIdent → TacticM Expr) : TacticM Expr

def Lean.Elab.Tactic.Do.ProofMode.elabMRefine : Tactic

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Tactic.Do.ProofMode.elabMExists : Tactic

Equations

• One or more equations did not get rendered due to their size.