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.SPred.mkType (u : Level) (σs : Expr) : Expr

def Lean.Elab.Tactic.Do.ProofMode.SPred.mkPure (u : Level) (σs p : Expr) : Expr

def Lean.Elab.Tactic.Do.ProofMode.SPred.isPure? : Expr → Option (Level × Expr × Expr)

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

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

def Lean.Elab.Tactic.Do.ProofMode.parseEmptyHyp? (e : Expr) : Option (Level × 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.SPred.mkAnd! (u : Level) (σ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.SPred.mkAnd (u : Level) (σ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.TypeList.mkType (u : Level) : Expr

def Lean.Elab.Tactic.Do.ProofMode.TypeList.mkNil (u : Level) : Expr

def Lean.Elab.Tactic.Do.ProofMode.TypeList.mkCons (u : Level) (hd tl : Expr) : Expr

def Lean.Elab.Tactic.Do.ProofMode.TypeList.length (σs : Expr) : MetaM Nat

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

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

• u : Level
• σs : Expr
• hyps : Expr
• target : Expr

def Lean.Elab.Tactic.Do.ProofMode.instInhabitedMGoal.default : MGoal

@[implicit_reducible]

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)

def Lean.Elab.Tactic.Do.ProofMode.checkHasType (expr expectedType : Expr) (suppressWarning : Bool := false) : MetaM Unit

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)

def Lean.Elab.Tactic.Do.ProofMode.pushForallContextIntoHyps (σs hyps : 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.MGoal.renameInaccessibleHyps (goal : MGoal) (idents : Array (TSyntax `Lean.binderIdent)) : MetaM MGoal

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