ink

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

• The hypothesis' BinderInfo

  binderInfo : Lean.BinderInfo

• The hypothesis' LocalDeclKind

  kind : Lean.LocalDeclKind

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

ink

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.