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

Equations

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

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.

Equations

• g.note h v (some t) = do let __do_lift ← pure t let __do_lift ← g.assert h __do_lift v __do_lift.intro1P
• g.note h v = do let __do_lift ← Lean.Meta.inferType v let __do_lift ← g.assert h __do_lift v __do_lift.intro1P

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

Equations

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

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

Equations

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

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.

Equations

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

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

Like Lean.MVarId.assertAfter, but asserts the new hypothesis at the earliest point after fvarId where type is well-formed. Note that val may depend on any variables in the local context.

The expression type may contain metavariables, and this procedure ensures they are well-formed at the point in the local context where the hypothesis is asserted. The metavariables in type are instantiated to avoid false dependencies.

Equations

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

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.

Equations

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