Similar to mkFreshUserName
, but takes into account tactic.hygienic
option value.
If tactic.hygienic = true
, then the current macro scopes are applied to binderName
.
If not, then an unused (accessible) name (based on binderName
) in the local context is used.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Introduce n
binders in the goal mvarId
.
Equations
- mvarId.introN n givenNames useNamesForExplicitOnly = Lean.Meta.introNCore mvarId n givenNames useNamesForExplicitOnly false
Instances For
Equations
- Lean.Meta.introN mvarId n givenNames useNamesForExplicitOnly = mvarId.introN n givenNames useNamesForExplicitOnly
Instances For
Introduce n
binders in the goal mvarId
. The new hypotheses are named using the binder names.
The suffix P
stands for "preserving`.
Equations
- mvarId.introNP n = Lean.Meta.introNCore mvarId n [] false true
Instances For
Equations
- Lean.Meta.introNP mvarId n = mvarId.introNP n
Instances For
Introduce one binder using name
as the the new hypothesis name.
Equations
Instances For
Equations
- Lean.Meta.intro mvarId name = mvarId.intro name
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Introduce one object from the goal mvarid
, without preserving the name used in the binder.
Returns a pair made of the newly introduced variable (which will have an inaccessible name)
and the new goal. This will fail if there is nothing to introduce, ie when the goal
does not start with a forall, lambda or let.
Equations
- mvarId.intro1 = Lean.Meta.intro1Core mvarId false
Instances For
Equations
- Lean.Meta.intro1 mvarId = mvarId.intro1
Instances For
Introduce one object from the goal mvarid
, preserving the name used in the binder.
Returns a pair made of the newly introduced variable and the new goal.
This will fail if there is nothing to introduce, ie when the goal
does not start with a forall, lambda or let.
Equations
- mvarId.intro1P = Lean.Meta.intro1Core mvarId true
Instances For
Equations
- Lean.Meta.intro1P mvarId = mvarId.intro1P
Instances For
Introduce as many binders as possible without unfolding definitions.
Equations
- One or more equations did not get rendered due to their size.