def Lean.MVarId.assert (mvarId : Lean.MVarId) (name : Lake.Name) (type : Lean.Expr) (val : Lean.Expr) : Lean.MetaM Lean.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 : Lean.MVarId) (h : Lake.Name) (v : Lean.Expr) (t? : optParam (Option Lean.Expr) none) : Lean.MetaM (Lean.FVarId × Lean.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 : Lean.MVarId) (name : Lake.Name) (type : Lean.Expr) (val : Lean.Expr) : Lean.MetaM Lean.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 : Lean.MVarId) (name : Lake.Name) (type : Lean.Expr) (val : Lean.Expr) (hName : optParam Lake.Name `h) : Lean.MetaM Lean.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 : Lean.FVarId
• mvarId : Lean.MVarId
• subst : Lean.Meta.FVarSubst

def Lean.MVarId.assertAfter (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (userName : Lake.Name) (type : Lean.Expr) (val : Lean.Expr) : Lean.MetaM Lean.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.

structure Lean.Meta.Hypothesis : Type

• userName : Lake.Name
• type : Lean.Expr
• value : Lean.Expr
• binderInfo : Lean.BinderInfo

  The hypothesis' BinderInfo

• kind : Lean.LocalDeclKind

  The hypothesis' LocalDeclKind

def Lean.MVarId.assertHypotheses (mvarId : Lean.MVarId) (hs : Array Lean.Meta.Hypothesis) : Lean.MetaM (Array Lean.FVarId × Lean.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.

def Lean.MVarId.replace (g : Lean.MVarId) (hyp : Lean.FVarId) (proof : Lean.Expr) (typeNew : optParam (Option Lean.Expr) none) : Lean.MetaM Lean.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.

Equations

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

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

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

Equations

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