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

    Instances For