The hypothesis'
BinderInfo
binderInfo : Lean.BinderInfoThe hypothesis'
LocalDeclKind
kind : Lean.LocalDeclKind
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.