structure Lean.Meta.Hypothesis'extends Lean.Meta.Hypothesis : Type

Description of a hypothesis for Lean.MVarId.assertHypotheses'.

• userName : Lean.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)

Add the given hypotheses to the local context. This is a generalisation of Lean.MVarId.assertHypotheses which lets you specify

Equations

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