@[match_pattern]

def Lean.Elab.Tactic.Do.ProofMode.nameAnnotation : Name

@[match_pattern]

def Lean.Elab.Tactic.Do.ProofMode.uniqAnnotation : Name

structure Lean.Elab.Tactic.Do.ProofMode.Hyp : Type

• name : Name
• uniq : Name
• p : Expr

def Lean.Elab.Tactic.Do.ProofMode.parseHyp? : Expr → Option Hyp

def Lean.Elab.Tactic.Do.ProofMode.Hyp.toExpr (hyp : Hyp) : Expr

def Lean.Elab.Tactic.Do.ProofMode.emptyHyp (σs : Expr) : Expr

def Lean.Elab.Tactic.Do.ProofMode.parseEmptyHyp? : Expr → Option Expr

def Lean.Elab.Tactic.Do.ProofMode.pushLeftConjunct (pos : SubExpr.Pos) : SubExpr.Pos

def Lean.Elab.Tactic.Do.ProofMode.pushRightConjunct (pos : SubExpr.Pos) : SubExpr.Pos

def Lean.Elab.Tactic.Do.ProofMode.mkAnd! (σs lhs rhs : Expr) : Expr

Combine two hypotheses into a conjunction. Precondition: Neither lhs nor rhs is empty (parseEmptyHyp?).

def Lean.Elab.Tactic.Do.ProofMode.mkAnd (σs lhs rhs : Expr) : Expr × Expr

Smart constructor that cancels away empty hypotheses, along with a proof that lhs ∧ rhs ⊣⊢ₛ result.

def Lean.Elab.Tactic.Do.ProofMode.σs.mkType : Expr

def Lean.Elab.Tactic.Do.ProofMode.σs.mkNil : Expr

def Lean.Elab.Tactic.Do.ProofMode.parseAnd? (e : Expr) : Option (Expr × Expr × Expr)

structure Lean.Elab.Tactic.Do.ProofMode.MGoal : Type

• σs : Expr
• hyps : Expr
• target : Expr

instance Lean.Elab.Tactic.Do.ProofMode.instInhabitedMGoal : Inhabited MGoal

def Lean.Elab.Tactic.Do.ProofMode.parseMGoal? (expr : Expr) : Option MGoal

def Lean.Elab.Tactic.Do.ProofMode.ensureMGoal : TacticM (MVarId × MGoal)

def Lean.Elab.Tactic.Do.ProofMode.MGoal.strip (goal : MGoal) : Expr

def Lean.Elab.Tactic.Do.ProofMode.MGoal.toExpr (goal : MGoal) : Expr

Roundtrips with parseMGoal?.

def Lean.Elab.Tactic.Do.ProofMode.MGoal.findHyp? (goal : MGoal) (name : Name) : Option (SubExpr.Pos × Hyp)

partial def Lean.Elab.Tactic.Do.ProofMode.MGoal.findHyp?.go (name : Name) (e : Expr) (p : SubExpr.Pos) : Option (SubExpr.Pos × Hyp)

def Lean.Elab.Tactic.Do.ProofMode.MGoal.checkProof (goal : MGoal) (prf : Expr) (suppressWarning : Bool := false) : MetaM Unit

def Lean.Elab.Tactic.Do.ProofMode.getFreshHypName : TSyntax `Lean.binderIdent → CoreM (Name × Syntax)

partial def Lean.Elab.Tactic.Do.ProofMode.betaRevPreservingHypNames (σs' e : Expr) (args : Array Expr) : Expr

def Lean.Elab.Tactic.Do.ProofMode.betaPreservingHypNames (σs' e : Expr) (args : Array Expr) : Expr

def Lean.Elab.Tactic.Do.ProofMode.dropStateList (σs : Expr) (n : Nat) : MetaM Expr

def Lean.Elab.Tactic.Do.ProofMode.addLocalVarInfo (stx : Syntax) (lctx : LocalContext) (expr : Expr) (expectedType? : Option Expr) (isBinder : Bool := false) : MetaM Unit

def Lean.Elab.Tactic.Do.ProofMode.addHypInfo (stx : Syntax) (σs : Expr) (hyp : Hyp) (isBinder : Bool := false) : MetaM Unit