Documentation

Lean.Meta.Tactic.Assert

source
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.
source
@[deprecated Lean.MVarId.assert]
def Lean.Meta.assert (mvarId : Lean.MVarId) (name : Lake.Name) (type : Lean.Expr) (val : Lean.Expr) :
Lean.MetaM Lean.MVarId
Equations
source
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
  • One or more equations did not get rendered due to their size.
source
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.
source
@[deprecated Lean.MVarId.define]
def Lean.Meta.define (mvarId : Lean.MVarId) (name : Lake.Name) (type : Lean.Expr) (val : Lean.Expr) :
Lean.MetaM Lean.MVarId
Equations
source
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.
source
@[deprecated Lean.MVarId.assertExt]
def Lean.Meta.assertExt (mvarId : Lean.MVarId) (name : Lake.Name) (type : Lean.Expr) (val : Lean.Expr) (hName : optParam Lake.Name `h) :
Lean.MetaM Lean.MVarId
Equations
source
structure Lean.Meta.AssertAfterResult :
Type
source
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.
source
@[deprecated Lean.MVarId.assertAfter]
def Lean.Meta.assertAfter (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (userName : Lake.Name) (type : Lean.Expr) (val : Lean.Expr) :
Lean.MetaM Lean.Meta.AssertAfterResult
Equations
source
structure Lean.Meta.Hypothesis :
Type
source
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.
source
@[deprecated Lean.MVarId.assertHypotheses]
def Lean.Meta.assertHypotheses (mvarId : Lean.MVarId) (hs : Array Lean.Meta.Hypothesis) :
Lean.MetaM (Array Lean.FVarId × Lean.MVarId)
Equations
source
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.
source
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.