Documentation

Std.Lean.Meta.AssertHypotheses

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.
    Instances For