def Lean.MVarId.assert (mvarId : MVarId) (name : Name) (type val : Expr) : MetaM MVarId

Convert the given goal Ctx |- target into Ctx |- type -> target. It assumes val has type type

def Lean.MVarId.note (g : MVarId) (h : Name) (v : Expr) (t? : Option Expr := none) : MetaM (FVarId × MVarId)

Add the hypothesis h : t, given v : t, and return the new FVarId.

def Lean.MVarId.define (mvarId : MVarId) (name : Name) (type val : Expr) : MetaM MVarId

Convert the given goal Ctx |- target into Ctx |- let name : type := val; target. It assumes val has type type

def Lean.MVarId.assertExt (mvarId : MVarId) (name : Name) (type val : Expr) (hName : Name := `h) : MetaM MVarId

Convert the given goal Ctx |- target into Ctx |- (hName : type) -> hName = val -> target. It assumes val has type type

structure Lean.Meta.AssertAfterResult : Type

• fvarId : FVarId
• mvarId : MVarId
• subst : FVarSubst

def Lean.MVarId.assertAfter (mvarId : MVarId) (fvarId : FVarId) (userName : Name) (type val : Expr) : MetaM Meta.AssertAfterResult

Convert the given goal Ctx |- target into a goal containing (userName : type) after the local declaration with if fvarId. It assumes val has type type, and that type is well-formed after fvarId. Note that val does not need to be well-formed after fvarId. That is, it may contain variables that are defined after fvarId.

structure Lean.Meta.Hypothesis : Type

• userName : Name
• type : Expr
• value : Expr
• binderInfo : BinderInfo

  The hypothesis' BinderInfo

• kind : LocalDeclKind

  The hypothesis' LocalDeclKind

def Lean.MVarId.assertHypotheses (mvarId : MVarId) (hs : Array Meta.Hypothesis) : MetaM (Array FVarId × MVarId)

Convert the given goal Ctx |- target into Ctx, (hs[0].userName : hs[0].type) ... |-target. It assumes hs[i].val has type hs[i].type.

def Lean.MVarId.replace (g : MVarId) (hyp : FVarId) (proof : Expr) (typeNew : Option Expr := none) : MetaM Meta.AssertAfterResult

Replace hypothesis hyp in goal g with proof : typeNew. The new hypothesis is given the same user name as the original, it attempts to avoid reordering hypotheses, and the original is cleared if possible.

def Lean.MVarId.replace.findMaxFVar (e : Expr) : StateRefT' IO.RealWorld LocalDecl MetaM Unit

Finds the LocalDecl for the FVar in e with the highest index.