Similar to Lean.Core.mkFreshUserName
, but takes into account the tactic.hygienic
option value.
If tactic.hygienic = true
, then fresh macro scopes are applied to binderName
.
If not, then returns an (accessible) name based on binderName
that is unused in the local context.
Equations
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
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
Instances For
Calculate the number of new hypotheses that would be created by intros
,
i.e. the number of binders which can be introduced without unfolding definitions.