- userName : Lean.Name
- type : Lean.Expr
- value : Lean.Expr
- binderInfo : Lean.BinderInfo
The hypothesis'
BinderInfo
- kind : Lean.LocalDeclKind
The hypothesis'
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