source
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

Instances For

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

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

Instances For

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

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

Instances For