Documentation

Lean.Meta.Tactic.Assert

source
def Lean.Meta.assert (mvarId : Lean.MVarId) (name : Lean.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
def Lean.Meta.define (mvarId : Lean.MVarId) (name : Lean.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
def Lean.Meta.assertExt (mvarId : Lean.MVarId) (name : Lean.Name) (type : Lean.Expr) (val : Lean.Expr) (hName : optParam Lean.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
structure Lean.Meta.AssertAfterResult:
Type
source
def Lean.Meta.assertAfter (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (userName : Lean.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
structure Lean.Meta.Hypothesis:
Type
source
def Lean.Meta.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.