# Documentation

Std.Lean.Meta.AssertHypotheses

structure Lean.Meta.Hypothesis'extends :

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

Instances For

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.